Move one method from ModelChecker to Exploration

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 8804000..5aa7399 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -220,7 +220,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
                get_exploration()->get_record_trace().to_string().c_str());
       exploration_->log_state();
 
-      this->exit(SIMGRID_MC_EXIT_SAFETY);
+      exploration_->system_exit(SIMGRID_MC_EXIT_SAFETY);
 
     default:
       xbt_die("Unexpected message from model-checked application");
@@ -228,13 +228,6 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
   return true;
 }
 
-/** Terminate the model-checker application */
-void ModelChecker::exit(int status)
-{
-  get_exploration()->get_remote_app().shutdown();
-  ::exit(status);
-}
-
 void ModelChecker::handle_waitpid()
 {
   XBT_DEBUG("Check for wait event");
@@ -263,7 +256,7 @@ void ModelChecker::handle_waitpid()
         if (WIFSIGNALED(status)) {
           MC_report_crash(exploration_, status);
           this->get_remote_process_memory().terminate();
-          this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+          exploration_->system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
       }
 #endif
@@ -283,7 +276,7 @@ void ModelChecker::handle_waitpid()
       else if (WIFSIGNALED(status)) {
         MC_report_crash(exploration_, status);
         this->get_remote_process_memory().terminate();
-        this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+        exploration_->system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
       } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
         this->get_remote_process_memory().terminate();

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 5554144..16fdee4 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -37,9 +37,6 @@ public:
   /** Let the application take a transition. A new Transition is created iff the last parameter is true */
   Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
 
-  /* Interactions with the simcall observer */
-  XBT_ATTRIB_NORETURN void exit(int status);
-
   Exploration* get_exploration() const { return exploration_; }
   void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index d60839c..cc76198 100644 (file)
--- a/src/mc/explo/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -209,7 +209,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
       XBT_INFO("*********************************************************");
       XBT_INFO("%s", send_diff.c_str());
       exploration_.log_state();
-      mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+      exploration_.system_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
       XBT_INFO("****************************************************");
       XBT_INFO("***** Non-deterministic communications pattern *****");
@@ -219,7 +219,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
       if (not recv_diff.empty())
         XBT_INFO("%s", recv_diff.c_str());
       exploration_.log_state();
-      mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
+      exploration_.system_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     }
   }
 }

diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp
index 773438b..e4e5639 100644 (file)
--- a/src/mc/explo/Exploration.cpp
+++ b/src/mc/explo/Exploration.cpp
@@ -57,4 +57,10 @@ void Exploration::log_state()
   }
 }
 
+void Exploration::system_exit(int status)
+{
+  get_remote_app().shutdown();
+  ::exit(status);
+}
+
 }; // namespace simgrid::mc

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index c1abd5b..ca06472 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -43,6 +43,9 @@ public:
   /** Main function of this algorithm */
   virtual void run() = 0;
 
+  /** Kill the application and the model-checker (which exits with `status`)*/
+  XBT_ATTRIB_NORETURN void system_exit(int status);
+
   /* These methods are callbacks called by the model-checking engine
    * to get and display information about the current state of the
    * model-checking algorithm: */