-void DFSExplorer::check_non_termination(const State* current_state)
-{
-#if SIMGRID_HAVE_STATEFUL_MC
- for (auto const& state : stack_) {
- if (state->get_system_state()->equals_to(*current_state->get_system_state(),
- *get_remote_app().get_remote_process_memory())) {
- XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
- XBT_INFO("******************************************");
- XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
- XBT_INFO("******************************************");
- XBT_INFO("Counter-example execution trace:");
- for (auto const& s : get_textual_trace())
- XBT_INFO(" %s", s.c_str());
- XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
- "--cfg=model-check/replay:'%s'",
- get_record_trace().to_string().c_str());
- log_state();
-
- throw McError(ExitStatus::NON_TERMINATION);
- }
- }
-#endif
-}
-