From ff96c45809a06f045655a0b8203e193349890a1b Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 18 Oct 2012 21:53:30 +0200 Subject: [PATCH] model-checker : backtracking if there is no request to execute --- src/mc/mc_liveness.c | 114 ------------------------------------------- 1 file changed, 114 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index f1e5e3dd08..f8757046c7 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -510,120 +510,6 @@ void MC_ddfs(int search_cycle){ } - }else{ /*No request to execute, search evolution in Büchi automaton */ - - MC_SET_RAW_MEM; - - /* Create the new expanded graph_state */ - next_graph_state = MC_state_pair_new(); - - xbt_dynar_reset(successors); - - MC_UNSET_RAW_MEM; - - - cursor= 0; - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - - res = MC_automaton_evaluate_label(transition_succ->label); - - if(res == 1){ // enabled transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } - - } - - cursor = 0; - - xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){ - - res = MC_automaton_evaluate_label(transition_succ->label); - - if(res == 2){ // true transition in automaton - MC_SET_RAW_MEM; - next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state)); - xbt_dynar_push(successors, &next_pair); - MC_UNSET_RAW_MEM; - } - - } - - cursor = 0; - - xbt_dynar_foreach(successors, cursor, pair_succ){ - - if(search_cycle == 1){ - - if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){ - - if(reached(pair_succ->automaton_state)){ - - XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); - - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("| ACCEPTANCE CYCLE |"); - XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); - XBT_INFO("Counter-example that violates formula :"); - MC_show_stack_liveness(mc_stack_liveness); - MC_dump_stack_liveness(mc_stack_liveness); - MC_print_statistics_pairs(mc_stats_pair); - exit(0); - - }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)); - - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; - - MC_ddfs(search_cycle); - - } - - }else{ - - MC_SET_RAW_MEM; - xbt_fifo_unshift(mc_stack_liveness, pair_succ); - MC_UNSET_RAW_MEM; - - MC_ddfs(search_cycle); - - } - - - }else{ - - if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - - set_pair_reached(pair_succ->automaton_state); - - search_cycle = 1; - - 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_ddfs(search_cycle); - - } - - /* Restore system before checking others successors */ - if(cursor != xbt_dynar_length(successors) - 1) - MC_replay_liveness(mc_stack_liveness, 1); - - - } - } }else{ -- 2.20.1