- 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){
- if((search_cycle == 1) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- MC_SET_RAW_MEM;
- MC_take_snapshot(snapshot);
- MC_UNSET_RAW_MEM;
-
- if(reached(a, pair_succ->automaton_state, snapshot) == 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);
- //MC_exit_liveness();
- exit(1);
- }
- }
-
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
- MC_UNSET_RAW_MEM;
-
- //XBT_DEBUG("Stack size before : %d", xbt_fifo_size(mc_stack_liveness_stateless));
-
- MC_ddfs_stateless(a, search_cycle, 0);
-
- //XBT_DEBUG("Stack size after : %d", xbt_fifo_size(mc_stack_liveness_stateless));
-
-
- if((search_cycle == 0) && ((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);
-
- MC_SET_RAW_MEM;
- MC_take_snapshot(snapshot);
- MC_UNSET_RAW_MEM;
-
- int pr = set_pair_reached(a, pair_succ->automaton_state, snapshot);
-
-
- /* pair shifted from stack when first MC_ddfs finished and returned at this point */
- MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
- MC_UNSET_RAW_MEM;