From 25c8adc001703bcf1c761ae66001a4b0539dcf0e Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sat, 16 Mar 2013 18:25:32 +0100 Subject: [PATCH] model-checker : add state equality reduction in ddfs algorithm --- src/mc/mc_liveness.c | 65 +++++++++++++++++++++++++++++++------------- 1 file changed, 46 insertions(+), 19 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 9b8e3616e6..06265cb6e0 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -712,46 +712,73 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); + if(visited(pair_succ->automaton_state)){ + + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ + + XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id); - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); + + } } }else{ + + if(visited(pair_succ->automaton_state)){ + + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); + + } } }else{ - if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ + if(visited(pair_succ->automaton_state)){ + + XBT_DEBUG("Next pair already visited !"); + break; + + }else{ + + if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - set_pair_reached(pair_succ->automaton_state); + set_pair_reached(pair_succ->automaton_state); - search_cycle = 1; + search_cycle = 1; - XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - } + } - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; + MC_SET_RAW_MEM; + xbt_fifo_unshift(mc_stack_liveness, pair_succ); + MC_UNSET_RAW_MEM; - MC_ddfs(search_cycle); + MC_ddfs(search_cycle); + + } } -- 2.20.1