- next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
- MC_take_snapshot(next_snapshot);
+ 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);
+ xbt_abort();
+
+ }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);
+
+ }
+