From 6988d9960f1104aaac5371c51c0d79daf1a13b68 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 4 Nov 2011 16:13:42 +0100 Subject: [PATCH] =?utf8?q?model-checker=20:=20last=20version=20(incorrect)?= =?utf8?q?=20of=20double=20dfs=20algorithm=20for=20liveness=20properties?= =?utf8?q?=20before=20major=20rewrite=20to=20correct=20an=20error=20in=20t?= =?utf8?q?he=20behavior=20of=20MC=20(possible=20evolution=20in=20B=C3=BCch?= =?utf8?q?i=20automaton=20untreated)?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- src/mc/mc_global.c | 3 ++- src/mc/mc_liveness.c | 22 +++++++++++++--------- 2 files changed, 15 insertions(+), 10 deletions(-) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 2738d46e43..ccbd0e0b6b 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -328,7 +328,8 @@ void MC_replay_liveness(xbt_fifo_t stack) /* Update statistics */ mc_stats_pair->visited_pairs++; - } + } + XBT_DEBUG("**** End Replay ****"); } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index fd73ea4ff2..9771381e78 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -304,8 +304,7 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle); XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state)); - - + mc_stats_pair->visited_pairs++; @@ -402,9 +401,9 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ - if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (MC_state_interleave_size(pair_succ->graph_state) > 0)){ + if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) ){ - //XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1); MC_SET_RAW_MEM; MC_take_snapshot(snapshot); @@ -422,21 +421,26 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){ } } + int interleave = MC_state_interleave_size(pair_succ->graph_state); + + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){ + XBT_DEBUG("Take snapshot of acceptance pair (depth = %d)", xbt_fifo_size(mc_stack_liveness_stateless) + 1 ); + MC_SET_RAW_MEM; + MC_take_snapshot(snapshot); + MC_UNSET_RAW_MEM; + } + MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ); MC_UNSET_RAW_MEM; - MC_ddfs_stateless(a, search_cycle, 0); /* If pair_succ is the last state of the execution (0 interleave), no acceptance cycle possible */ - if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (MC_state_interleave_size(pair_succ->graph_state) > 0)){ + if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && ( interleave > 0)){ XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); - MC_SET_RAW_MEM; - MC_take_snapshot(snapshot); - MC_UNSET_RAW_MEM; set_pair_reached(a, pair_succ->automaton_state, snapshot); -- 2.20.1