MC: simplify initialization and kill api::set_checker()

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index eba0ac6..6831053 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -3,6 +3,7 @@
 #include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
 #include "src/mc/Session.hpp"
+#include "src/mc/checker/Checker.hpp"
 #include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_comm_pattern.hpp"
 #include "src/mc/mc_exit.hpp"
@@ -383,7 +384,7 @@ std::string Api::get_actor_dot_label(smx_actor_t actor) const
   return res;
 }
 
-void Api::initialize(char** argv) const
+simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
 {
   simgrid::mc::session = new simgrid::mc::Session([argv] {
     int i = 1;
@@ -394,6 +395,31 @@ void Api::initialize(char** argv) const
     execvp(argv[i], argv + i);
     xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
   });
+
+  simgrid::mc::Checker* checker;
+  switch (algo) {
+    case CheckerAlgorithm::CommDeterminism:
+      checker = simgrid::mc::createCommunicationDeterminismChecker();
+      break;
+
+    case CheckerAlgorithm::UDPOR:
+      checker = simgrid::mc::createUdporChecker();
+      break;
+
+    case CheckerAlgorithm::Safety:
+      checker = simgrid::mc::createSafetyChecker();
+      break;
+
+    case CheckerAlgorithm::Liveness:
+      checker = simgrid::mc::createLivenessChecker();
+      break;
+
+    default:
+      THROW_IMPOSSIBLE;
+  }
+
+  mc_model_checker->setChecker(checker);
+  return checker;
 }
 
 std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
@@ -613,13 +639,6 @@ Checker* Api::mc_get_checker() const
   return mc_model_checker->getChecker();
 }
 
-void Api::set_checker(Checker* const checker) const
-{
-  xbt_assert(mc_model_checker);
-  xbt_assert(mc_model_checker->getChecker() == nullptr);
-  mc_model_checker->setChecker(checker);
-}
-
 void Api::handle_simcall(Transition const& transition) const
 {
   mc_model_checker->handle_simcall(transition);

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 07ec4be..792af3f 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -15,6 +15,8 @@
 namespace simgrid {
 namespace mc {
 
+XBT_DECLARE_ENUM_CLASS(CheckerAlgorithm, Safety, UDPOR, Liveness, CommDeterminism);
+
 /**
  * @brief Maintains the transition's information.
  */
@@ -64,7 +66,7 @@ public:
     return api;
   }
 
-  void initialize(char** argv) const;
+  simgrid::mc::Checker* initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const;
 
   // ACTOR APIs
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
@@ -97,7 +99,6 @@ public:
   void mc_check_deadlock() const;
   bool mc_is_null() const;
   Checker* mc_get_checker() const;
-  void set_checker(Checker* const checker) const;
   void handle_simcall(Transition const& transition) const;
   void mc_wait_for_requests() const;
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;

diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp
index cf63b20..1fe6c64 100644 (file)
--- a/src/mc/checker/Checker.hpp
+++ b/src/mc/checker/Checker.hpp
@@ -27,7 +27,7 @@ namespace mc {
 // abstract
 class Checker {
 public:
-  inline explicit Checker() { Api::get().set_checker(this); }
+  explicit Checker() = default;
 
   // No copy:
   Checker(Checker const&) = delete;

diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp
index 455290e..f91ef2b 100644 (file)
--- a/src/mc/checker/simgrid_mc.cpp
+++ b/src/mc/checker/simgrid_mc.cpp
@@ -29,18 +29,6 @@ char** argvdup(int argc, char** argv)
   return argv_copy;
 }
 
-static std::unique_ptr<simgrid::mc::Checker> create_checker()
-{
-  if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
-    return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createCommunicationDeterminismChecker());
-  else if (_sg_mc_unfolding_checker)
-    return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createUdporChecker());
-  else if (_sg_mc_property_file.get().empty())
-    return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createSafetyChecker());
-  else
-    return std::unique_ptr<simgrid::mc::Checker>(simgrid::mc::createLivenessChecker());
-}
-
 int main(int argc, char** argv)
 {
   if (argc < 2)
@@ -52,16 +40,25 @@ int main(int argc, char** argv)
   // The initialization function can touch argv.
   // We make a copy of argv before modifying it in order to pass the original value to the model-checked application:
   char** argv_copy = argvdup(argc, argv);
+
   xbt_log_init(&argc, argv);
 #if HAVE_SMPI
   smpi_init_options(); // only performed once
 #endif
   sg_config_init(&argc, argv);
-  api::get().initialize(argv_copy);
-  delete[] argv_copy;
 
-  auto checker = create_checker();
+  simgrid::mc::CheckerAlgorithm algo;
+  if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+    algo = simgrid::mc::CheckerAlgorithm::CommDeterminism;
+  else if (_sg_mc_unfolding_checker)
+    algo = simgrid::mc::CheckerAlgorithm::UDPOR;
+  else if (_sg_mc_property_file.get().empty())
+    algo = simgrid::mc::CheckerAlgorithm::Safety;
+  else
+    algo = simgrid::mc::CheckerAlgorithm::Liveness;
+
   int res      = SIMGRID_MC_EXIT_SUCCESS;
+  auto checker = api::get().initialize(argv_copy, algo);
   try {
     checker->run();
   } catch (const simgrid::mc::DeadlockError&) {
@@ -73,5 +70,6 @@ int main(int argc, char** argv)
   }
   checker = nullptr;
   api::get().s_close();
+  delete[] argv_copy;
   return res;
 }