X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f67180bbc092450879b291aa18be74801b30b240..09abefeb928cd7ea4679407a6b4387d4f75beaa9:/src/mc/api.cpp

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index eba0ac6adc..f95a8b2b7c 100644
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -3,12 +3,13 @@
 #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"
 #include "src/mc/mc_pattern.hpp"
 #include "src/mc/mc_private.hpp"
-#include "src/mc/remote/RemoteSimulation.hpp"
+#include "src/mc/remote/RemoteProcess.hpp"
 
 #include <xbt/asserts.h>
 #include <xbt/log.h>
@@ -332,7 +333,7 @@ xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
   if (mc_model_checker == nullptr)
     return actor->get_host()->get_name();
 
-  const simgrid::mc::RemoteSimulation* process = &mc_model_checker->get_remote_simulation();
+  const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_simulation();
 
   // Read the simgrid::xbt::string in the MCed process:
   simgrid::mc::ActorInformation* info = actor_info_cast(actor);
@@ -353,7 +354,7 @@ std::string Api::get_actor_name(smx_actor_t actor) const
 
   simgrid::mc::ActorInformation* info = actor_info_cast(actor);
   if (info->name.empty()) {
-    const simgrid::mc::RemoteSimulation* process = &mc_model_checker->get_remote_simulation();
+    const simgrid::mc::RemoteProcess* process = &mc_model_checker->get_remote_simulation();
 
     simgrid::xbt::string_data string_data = simgrid::xbt::string::to_string_data(actor->name_);
     info->name = process->read_string(remote(string_data.data), string_data.len);
@@ -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
@@ -514,7 +540,7 @@ smx_actor_t Api::get_dst_actor(RemotePtr<kernel::activity::CommImpl> const& comm
 
 std::size_t Api::get_remote_heap_bytes() const
 {
-  RemoteSimulation& process = mc_model_checker->get_remote_simulation();
+  RemoteProcess& process    = mc_model_checker->get_remote_simulation();
   auto heap_bytes_used      = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info());
   return heap_bytes_used;
 }
@@ -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);