-static int is_exploration_stack_state(mc_state_t current_state){
-
- xbt_fifo_item_t item;
- mc_state_t stack_state;
- for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
- stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
- if(snapshot_compare(stack_state, current_state) == 0){
- XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
- return 1;
- }
- }
- return 0;
+static void MC_show_non_termination(void)
+{
+ XBT_INFO("******************************************");
+ XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+ XBT_INFO("******************************************");
+ XBT_INFO("Counter-example execution trace:");
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
+ MC_print_statistics(mc_stats);