Remove more uses of the session global

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index b6cee6c..833c7df 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -455,11 +455,6 @@ std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
   return mc_model_checker->get_remote_process().actors();
 }
 
-bool Api::actor_is_enabled(aid_t pid) const
-{
-  return session->actor_is_enabled(pid);
-}
-
 unsigned long Api::get_maxpid() const
 {
   static const char* name = nullptr;

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 3e4f3e6..36730ee 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -69,7 +69,6 @@ public:
 
   // ACTOR APIs
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
-  bool actor_is_enabled(aid_t pid) const;
   unsigned long get_maxpid() const;
   int get_actors_size() const;
 

diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp
index ebc0448..c0ba4a3 100644 (file)
--- a/src/mc/checker/Checker.hpp
+++ b/src/mc/checker/Checker.hpp
@@ -55,7 +55,7 @@ public:
   /** Log additional information about the state of the model-checker */
   virtual void log_state() = 0;
 
-  Session* get_session() { return session_; }
+  Session& get_session() { return *session_; }
 };
 
 // External constructors so that the types (and the types of their content) remain hidden

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 9c179ab..6ae7e10 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -316,7 +316,7 @@ void CommunicationDeterminismChecker::prepare()
   /* Add all enabled actors to the interleave set of the initial state */
   for (auto& act : api::get().get_actors()) {
     auto actor = act.copy.get_buffer();
-    if (api::get().actor_is_enabled(actor->get_pid()))
+    if (get_session().actor_is_enabled(actor->get_pid()))
       initial_state->mark_todo(actor);
   }
 
@@ -471,7 +471,7 @@ void CommunicationDeterminismChecker::real_run()
         /* Add all enabled actors to the interleave set of the next state */
         for (auto& act : api::get().get_actors()) {
           auto actor = act.copy.get_buffer();
-          if (api::get().actor_is_enabled(actor->get_pid()))
+          if (get_session().actor_is_enabled(actor->get_pid()))
             next_state->mark_todo(actor);
         }
 
@@ -528,7 +528,7 @@ void CommunicationDeterminismChecker::real_run()
 void CommunicationDeterminismChecker::run()
 {
   XBT_INFO("Check communication determinism");
-  get_session()->take_initial_snapshot();
+  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 c3730a9..ebdddcf 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -259,7 +259,7 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
   /* Add all enabled actors to the interleave set of the initial state */
   for (auto& act : api::get().get_actors()) {
     auto actor = act.copy.get_buffer();
-    if (api::get().actor_is_enabled(actor->get_pid()))
+    if (get_session().actor_is_enabled(actor->get_pid()))
       next_pair->graph_state->mark_todo(actor);
   }
 
@@ -300,7 +300,7 @@ void LivenessChecker::run()
   api::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  get_session()->take_initial_snapshot();
+  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 cb8762a..2bc2bdb 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -147,7 +147,7 @@ void SafetyChecker::run()
       auto actors = api::get().get_actors(); 
       for (auto& remoteActor : actors) {
         auto actor = remoteActor.copy.get_buffer();
-        if (api::get().actor_is_enabled(actor->get_pid())) {
+        if (get_session().actor_is_enabled(actor->get_pid())) {
           next_state->mark_todo(actor);
           if (reductionMode_ == ReductionMode::dpor)
             break; // With DPOR, we take the first enabled transition
@@ -267,7 +267,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
              (reductionMode_ == ReductionMode::none ? "none"
                                                     : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
 
-  get_session()->take_initial_snapshot();
+  get_session().take_initial_snapshot();
 
   XBT_DEBUG("Starting the safety algorithm");
 
@@ -280,7 +280,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
   /* Get an enabled actor and insert it in the interleave set of the initial state */
   auto actors = api::get().get_actors();
   for (auto& actor : actors)
-    if (api::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
+    if (get_session().actor_is_enabled(actor.copy.get_buffer()->get_pid())) {
       initial_state->mark_todo(actor.copy.get_buffer());
       if (reductionMode_ != ReductionMode::none)
         break;