- }else{
-
- mc_stats->executed_transitions++;
-
- XBT_DEBUG("No request to execute in this state, search evolution in Büchi Automaton.");
-
- if(current_pair->search_cycle){
-
- if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
-
- if((reached_num = is_reached_acceptance_pair(current_pair)) != -1){
-
- XBT_INFO("Pair %d already reached (equal to pair %d) !", current_pair->num, reached_num);
-
- MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_stack_liveness);
- MC_UNSET_RAW_MEM;
-
- 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(mc_stats);
- xbt_abort();
-
- }
- }
- }
-
- if((visited_num = is_visited_pair(current_pair)) != -1){
-
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", current_pair->num, visited_num);
-
- }else{
-
- /* Evaluate enabled transition according to atomic propositions values */
- 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 = MC_pair_new();
- next_pair->graph_state = MC_state_new();
- next_pair->automaton_state = transition_succ->dst;
- next_pair->atomic_propositions = get_atomic_propositions_values();
- next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-
- if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
- next_pair->search_cycle = 1;
-
- xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
- if(mc_stats->expanded_pairs%1000 == 0)
- XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-
- MC_UNSET_RAW_MEM;
-
- MC_ddfs();
-
- MC_replay_liveness(mc_stack_liveness, 1);
-
- }
-
-
-
- }
-
- /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
- 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 = MC_pair_new();
- next_pair->graph_state = MC_state_new();
- next_pair->automaton_state = transition_succ->dst;
- next_pair->atomic_propositions = get_atomic_propositions_values();
- next_pair->requests = MC_state_interleave_size(next_pair->graph_state);
-
- if(next_pair->automaton_state->type == 1 || next_pair->automaton_state->type == 2 || current_pair->search_cycle)
- next_pair->search_cycle = 1;
-
- xbt_fifo_unshift(mc_stack_liveness, next_pair);
-
- if(mc_stats->expanded_pairs%1000 == 0)
- XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
-
- MC_UNSET_RAW_MEM;
-
- MC_ddfs();
-
- MC_replay_liveness(mc_stack_liveness, 1);
- }
-
- }
-
- if(MC_state_interleave_size(current_pair->graph_state) > 0){
- XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
- MC_replay_liveness(mc_stack_liveness, 0);
- }
-
- }