The checker has the session and don't need the API to interact with it

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 0bd6e82..77c68af 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -98,8 +98,8 @@ Session::~Session()
   this->close();
 }
 
-/** Take the initial snapshot of the application, that must be stopped. */
-void Session::initialize()
+/** The application must be stopped. */
+void Session::take_initial_snapshot()
 {
   xbt_assert(initial_snapshot_ == nullptr);
   model_checker_->wait_for_requests();

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index c0942d8..1f42a04 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -44,7 +44,7 @@ public:
   ~Session();
   void close();
 
-  void initialize();
+  void take_initial_snapshot();
   void execute(Transition const& transition) const;
   void log_state() const;
 

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 825edc5..ee58589 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -573,11 +573,6 @@ std::size_t Api::get_remote_heap_bytes() const
   return heap_bytes_used;
 }
 
-void Api::session_initialize() const
-{
-  session->initialize();
-}
-
 void Api::mc_inc_visited_states() const
 {
   mc_model_checker->visited_states++;
@@ -962,11 +957,6 @@ void Api::s_close() const
   session->close();
 }
 
-void Api::restore_initial_state() const
-{
-  session->restore_initial_state();
-}
-
 void Api::execute(Transition& transition, smx_simcall_t simcall) const
 {
   /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 7d05275..3e4f3e6 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -123,14 +123,12 @@ public:
   // STATE APIs
   void restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const;
   void log_state() const;
-  void restore_initial_state() const;
 
   // SNAPSHOT APIs
   bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
   simgrid::mc::Snapshot* take_snapshot(int num_state) const;
 
   // SESSION APIs
-  void session_initialize() const;
   void s_close() const;
   void execute(Transition& transition, smx_simcall_t simcall) const;
 

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 07db218..05eede3 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
 #include "src/kernel/activity/MailboxImpl.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -343,8 +344,7 @@ void CommunicationDeterminismChecker::restoreState()
     return;
   }
 
-  /* Restore the initial state */
-  api::get().restore_initial_state();
+  session->restore_initial_state();
 
   const unsigned long maxpid = api::get().get_maxpid();
   assert(maxpid == incomplete_communications_pattern.size());
@@ -526,7 +526,7 @@ void CommunicationDeterminismChecker::real_run()
 void CommunicationDeterminismChecker::run()
 {
   XBT_INFO("Check communication determinism");
-  api::get().session_initialize();
+  get_session()->take_initial_snapshot();
 
   this->prepare();
   this->real_run();

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 7b3c253..de70985 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -4,6 +4,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/checker/LivenessChecker.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -115,8 +116,7 @@ void LivenessChecker::replay()
     }
   }
 
-  /* Restore the initial state */
-  api::get().restore_initial_state();
+  session->restore_initial_state();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
@@ -298,7 +298,7 @@ void LivenessChecker::run()
   api::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  api::get().session_initialize();
+  get_session()->take_initial_snapshot();
 
   /* Initialize */
   this->previous_pair_ = 0;

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 4c3c0d2..cb8762a 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -13,6 +13,7 @@
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
+#include "src/mc/Session.hpp"
 #include "src/mc/Transition.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/checker/SafetyChecker.hpp"
@@ -238,8 +239,7 @@ void SafetyChecker::restore_state()
     return;
   }
 
-  /* Restore the initial state */
-  api::get().restore_initial_state();
+  session->restore_initial_state();
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (std::unique_ptr<State> const& state : stack_) {
@@ -266,8 +266,8 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
     XBT_INFO("Check a safety property. Reduction is: %s.",
              (reductionMode_ == ReductionMode::none ? "none"
                                                     : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
-  
-  api::get().session_initialize();  
+
+  get_session()->take_initial_snapshot();
 
   XBT_DEBUG("Starting the safety algorithm");