One less global variable: session_singleton.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 4d7be7f..75024f6 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
 #include "src/mc/explo/Exploration.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
@@ -140,7 +139,7 @@ static void MC_report_crash(int status)
     for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace())
       XBT_INFO("  %s", s.c_str());
     XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
-    session_singleton->log_state();
+    Api::get().get_session().log_state();
     if (xbt_log_no_loc) {
       XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
     } else {
@@ -232,7 +231,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
       XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
-      session_singleton->log_state();
+      Api::get().get_session().log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index e8b1726..3e0fb61 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -176,7 +176,5 @@ void Session::check_deadlock() const
     throw DeadlockError();
   }
 }
-
-std::unique_ptr<simgrid::mc::Session> session_singleton;
 }
 }

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 4c0269c..520cbbf 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -55,9 +55,6 @@ public:
 
   bool actor_is_enabled(aid_t pid) const;
 };
-
-// Temporary :)
-extern std::unique_ptr<simgrid::mc::Session> session_singleton;
 }
 }
 

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 450b95a..0fd826c 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -48,9 +48,9 @@ static simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor)
   return process_info;
 }
 
-simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
+simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo)
 {
-  simgrid::mc::session_singleton = std::make_unique<simgrid::mc::Session>([argv] {
+  session_ = std::make_unique<simgrid::mc::Session>([argv] {
     int i = 1;
     while (argv[i] != nullptr && argv[i][0] == '-')
       i++;
@@ -63,19 +63,19 @@ simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgor
   simgrid::mc::Exploration* explo;
   switch (algo) {
     case CheckerAlgorithm::CommDeterminism:
-      explo = simgrid::mc::create_communication_determinism_checker(session_singleton.get());
+      explo = simgrid::mc::create_communication_determinism_checker(session_.get());
       break;
 
     case CheckerAlgorithm::UDPOR:
-      explo = simgrid::mc::create_udpor_checker(session_singleton.get());
+      explo = simgrid::mc::create_udpor_checker(session_.get());
       break;
 
     case CheckerAlgorithm::Safety:
-      explo = simgrid::mc::create_safety_checker(session_singleton.get());
+      explo = simgrid::mc::create_safety_checker(session_.get());
       break;
 
     case CheckerAlgorithm::Liveness:
-      explo = simgrid::mc::create_liveness_checker(session_singleton.get());
+      explo = simgrid::mc::create_liveness_checker(session_.get());
       break;
 
     default:
@@ -134,10 +134,9 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
   return snapshot;
 }
 
-void Api::s_close() const
+void Api::s_close()
 {
-  session_singleton->close();
-  session_singleton.reset();
+  session_.reset();
   if (simgrid::mc::property_automaton != nullptr) {
     xbt_automaton_free(simgrid::mc::property_automaton);
     simgrid::mc::property_automaton = nullptr;

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 4c36702..f11f70f 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -10,6 +10,7 @@
 #include <vector>
 
 #include "simgrid/forward.h"
+#include "src/mc/Session.hpp"
 #include "src/mc/api/State.hpp"
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/mc_record.hpp"
@@ -40,6 +41,8 @@ private:
     }
   };
 
+  std::unique_ptr<simgrid::mc::Session> session_;
+
 public:
   // No copy:
   Api(Api const&) = delete;
@@ -51,7 +54,7 @@ public:
     return api;
   }
 
-  simgrid::mc::Exploration* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const;
+  simgrid::mc::Exploration* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo);
 
   // ACTOR APIs
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
@@ -73,9 +76,10 @@ public:
   simgrid::mc::Snapshot* take_snapshot(long num_state) const;
 
   // SESSION APIs
-  void s_close() const;
+  simgrid::mc::Session const& get_session() { return *session_; }
+  void s_close();
 
-// AUTOMATION APIs
+  // AUTOMATION APIs
   void automaton_load(const char* file) const;
   std::vector<int> automaton_propositional_symbol_evaluate() const;
   std::vector<xbt_automaton_state_t> get_automaton_state() const;

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index accf6d5..eba88b3 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/api/State.hpp"
-#include "src/mc/Session.hpp"
 #include "src/mc/api.hpp"
 #include "src/mc/mc_config.hpp"
 
@@ -50,7 +49,7 @@ int State::next_transition() const
     const ActorState* actor_state = &actor_states_[aid];
 
     /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/
-    if (not actor_state->is_todo() || not simgrid::mc::session_singleton->actor_is_enabled(aid))
+    if (not actor_state->is_todo() || not Api::get().get_session().actor_is_enabled(aid))
       continue;
 
     return i;

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index 1e29c81..ba1af71 100644 (file)
--- a/src/mc/explo/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/kernel/activity/MailboxImpl.hpp"
-#include "src/mc/Session.hpp"
 #include "src/mc/explo/SafetyChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
@@ -206,7 +205,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
       XBT_INFO("***** Non-send-deterministic communications pattern *****");
       XBT_INFO("*********************************************************");
       XBT_INFO("%s", send_diff.c_str());
-      session_singleton->log_state();
+      Api::get().get_session().log_state();
       Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
       XBT_INFO("****************************************************");
@@ -216,7 +215,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
         XBT_INFO("%s", send_diff.c_str());
       if (not recv_diff.empty())
         XBT_INFO("%s", recv_diff.c_str());
-      session_singleton->log_state();
+      Api::get().get_session().log_state();
       Api::get().mc_exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     }
   }

diff --git a/src/mc/explo/SafetyChecker.cpp b/src/mc/explo/SafetyChecker.cpp
index 9bcf5ad..6441a73 100644 (file)
--- a/src/mc/explo/SafetyChecker.cpp
+++ b/src/mc/explo/SafetyChecker.cpp
@@ -4,7 +4,6 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/explo/SafetyChecker.hpp"
-#include "src/mc/Session.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
@@ -192,7 +191,7 @@ void SafetyChecker::backtrack()
   on_backtracking_signal();
   stack_.pop_back();
 
-  session_singleton->check_deadlock();
+  get_session().check_deadlock();
 
   /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
    *  have it empty in the way. For each deleted state, check if the request that has generated it (from its