Add reference to parent state: only use this creation in DFSexplorer

[simgrid.git] / src / mc / ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 3f8db6157e6837899bda6c93458a3fae7a32e43d..10f0ba30c6fcb107a63a40744b4ea8f2525d3f8f 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -69,8 +69,6 @@ void ModelChecker::start()
   xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
              "Could not wait model-checked process");
 
-  setup_ignore();
-
   errno = 0;
 #ifdef __linux__
   ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
@@ -87,24 +85,6 @@ void ModelChecker::start()
              errno);
 }
 
-static constexpr auto ignored_local_variables = {
-    std::make_pair("e", "*"),
-    std::make_pair("_log_ev", "*"),
-
-    /* Ignore local variable about time used for tracing */
-    std::make_pair("start_time", "*"),
-};
-
-void ModelChecker::setup_ignore()
-{
-  const RemoteProcessMemory& process = this->get_remote_process_memory();
-  for (auto const& [var, frame] : ignored_local_variables)
-    process.ignore_local_variable(var, frame);
-
-  /* Static variable used for tracing */
-  process.ignore_global_variable("counter");
-}
-
 bool ModelChecker::handle_message(const char* buffer, ssize_t size)
 {
   s_mc_message_t base_message;
@@ -174,17 +154,8 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       return false;
 
     case MessageType::ASSERTION_FAILED:
-      XBT_INFO("**************************");
-      XBT_INFO("*** PROPERTY NOT VALID ***");
-      XBT_INFO("**************************");
-      XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : get_exploration()->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_exploration()->get_record_trace().to_string().c_str());
-      exploration_->log_state();
-      exploration_->system_exit(SIMGRID_MC_EXIT_SAFETY);
+      exploration_->report_assertion_failure();
+      break;
 
     default:
       xbt_die("Unexpected message from model-checked application");