- if(is_reached_acceptance_pair(pair_succ->num, pair_succ->automaton_state) != -1){
-
- 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(mc_stats);
- xbt_abort();
-
- }else{
-
- if(is_visited_pair(pair_succ->num, pair_succ->automaton_state) != -1){
-
- XBT_DEBUG("Next pair already visited !");
- break;
-
- }else{
-
- XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
-
- XBT_INFO("Acceptance pairs : %lu", xbt_dynar_length(acceptance_pairs));