- snap = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(snap);
-
- MC_UNSET_RAW_MEM;
-
- //xbt_dynar_reset(successors);
-
- cursor = 0;
-
- xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
-
- res = MC_automaton_evaluate_label(a, transition_succ->label);
-
- MC_SET_RAW_MEM;
-
- if((res == 1) || (res == 2)){ // enabled transition in automaton
- next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
- xbt_dynar_push(successors, &next_pair);
- }
-
- MC_UNSET_RAW_MEM;
- }
-
-
- if(xbt_dynar_length(successors) == 0){
-
- MC_SET_RAW_MEM;
- next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
- xbt_dynar_push(successors, &next_pair);
- MC_UNSET_RAW_MEM;
-
- }
-
- cursor = 0;
-
- xbt_dynar_foreach(successors, cursor, pair_succ){
-
- mc_reached_pair_stateless_t p = NULL;
- p = xbt_new0(s_mc_reached_pair_stateless_t, 1);
- p->pair = pair_succ;
- p->snapshot_system = snap;
-
- if((search_cycle == 1) && (reached_stateless(p) == 1)){
- XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
- XBT_INFO("| ACCEPTANCE CYCLE |");
- XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
- XBT_INFO("Counter-example that violates formula :");
- MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
- MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
- MC_print_statistics_pairs(mc_stats_pair);
- exit(0);
- }
-
- mc_stats_pair->executed_transitions++;
-
- 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((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
-
- set_pair_stateless_reached(current_pair);
- XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
- MC_replay_liveness(mc_stack_liveness_stateless);
- MC_ddfs_stateless(a, 1, 1);