Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Give an explicit name to the session singleton
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 14 Mar 2021 02:14:35 +0000 (03:14 +0100)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Sun, 14 Mar 2021 02:16:06 +0000 (03:16 +0100)
src/mc/ModelChecker.cpp
src/mc/Session.cpp
src/mc/Session.hpp
src/mc/api.cpp
src/mc/checker/CommunicationDeterminismChecker.cpp
src/mc/checker/LivenessChecker.cpp
src/mc/checker/SafetyChecker.cpp
src/mc/mc_base.cpp
src/mc/mc_global.cpp

index e2fa183..198b920 100644 (file)
@@ -138,7 +138,7 @@ static void MC_report_crash(int status)
   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   dumpRecordPath();
-  session->log_state();
+  session_singleton->log_state();
   if (xbt_log_no_loc) {
     XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
   } else {
@@ -220,7 +220,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       for (auto const& s : getChecker()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
       dumpRecordPath();
-      session->log_state();
+      session_singleton->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 
index 77c68af..fe6b08a 100644 (file)
@@ -154,7 +154,6 @@ bool Session::actor_is_enabled(aid_t pid) const
   return ((s_mc_message_int_t*)buff.data())->value;
 }
 
-simgrid::mc::Session* session;
-
+simgrid::mc::Session* session_singleton;
 }
 }
index 1f42a04..d89b702 100644 (file)
@@ -53,8 +53,7 @@ public:
 };
 
 // Temporary :)
-extern simgrid::mc::Session* session;
-
+extern simgrid::mc::Session* session_singleton;
 }
 }
 
index 833c7df..cb0d23e 100644 (file)
@@ -414,7 +414,7 @@ std::string Api::get_actor_dot_label(smx_actor_t actor) const
 
 simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
 {
-  simgrid::mc::session = new simgrid::mc::Session([argv] {
+  auto session = new simgrid::mc::Session([argv] {
     int i = 1;
     while (argv[i] != nullptr && argv[i][0] == '-')
       i++;
@@ -446,6 +446,7 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm
       THROW_IMPOSSIBLE;
   }
 
+  simgrid::mc::session_singleton = session;
   mc_model_checker->setChecker(checker);
   return checker;
 }
@@ -933,7 +934,7 @@ void Api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) con
 
 void Api::log_state() const
 {
-  session->log_state();
+  session_singleton->log_state();
 }
 
 bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
@@ -949,14 +950,14 @@ simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const
 
 void Api::s_close() const
 {
-  session->close();
+  session_singleton->close();
 }
 
 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() */
   transition.textual = request_to_string(simcall, transition.times_considered_);
-  session->execute(transition);
+  session_singleton->execute(transition);
 }
 
 void Api::automaton_load(const char* file) const
index 6ae7e10..276fd77 100644 (file)
@@ -345,7 +345,7 @@ void CommunicationDeterminismChecker::restoreState()
     return;
   }
 
-  session->restore_initial_state();
+  get_session().restore_initial_state();
 
   const unsigned long maxpid = api::get().get_maxpid();
   assert(maxpid == incomplete_communications_pattern.size());
index ebdddcf..1c14baf 100644 (file)
@@ -116,7 +116,7 @@ void LivenessChecker::replay()
     }
   }
 
-  session->restore_initial_state();
+  get_session().restore_initial_state();
 
   /* Traverse the stack from the initial state and re-execute the transitions */
   int depth = 1;
index 2bc2bdb..c11b0fe 100644 (file)
@@ -239,7 +239,7 @@ void SafetyChecker::restore_state()
     return;
   }
 
-  session->restore_initial_state();
+  get_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_) {
index b456467..da5d3bf 100644 (file)
@@ -82,7 +82,7 @@ bool actor_is_enabled(smx_actor_t actor)
 #if SIMGRID_HAVE_MC
   // If in the MCer, ask the client app since it has all the data
   if (mc_model_checker != nullptr) {
-    return simgrid::mc::session->actor_is_enabled(actor->get_pid());
+    return simgrid::mc::session_singleton->actor_is_enabled(actor->get_pid());
   }
 #endif
 // #
index 70633f9..7370a9e 100644 (file)
@@ -88,7 +88,7 @@ void MC_show_deadlock()
   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
-  simgrid::mc::session->log_state();
+  simgrid::mc::session_singleton->log_state();
 }
 
 void MC_automaton_load(const char *file)