MC: move a function around + cosmetics

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index e679402..e9741ec 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -50,6 +50,7 @@ public:
   void handle_events(int fd, short events);
   void wait_for_requests();
   void handle_simcall(Transition const& transition);
+
   XBT_ATTRIB_NORETURN void exit(int status);
 
   bool checkDeadlock();

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 629505c..162dfc0 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -141,6 +141,16 @@ void Session::close()
   }
 }
 
+bool Session::actor_is_enabled(aid_t pid)
+{
+  s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
+  model_checker_->process().get_channel().send(msg);
+  char buff[MC_MESSAGE_LENGTH];
+  ssize_t received = model_checker_->process().get_channel().receive(buff, MC_MESSAGE_LENGTH, true);
+  xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED");
+  return ((s_mc_message_int_t*)buff)->value;
+}
+
 simgrid::mc::Session* session;
 
 }

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 06f12de..9f07bad 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -6,6 +6,7 @@
 #ifndef SIMGRID_MC_SESSION_HPP
 #define SIMGRID_MC_SESSION_HPP
 
+#include "simgrid/forward.h"
 #include "src/mc/ModelChecker.hpp"
 
 #include <functional>
@@ -48,6 +49,7 @@ public:
   void log_state();
 
   void restore_initial_state();
+  bool actor_is_enabled(aid_t pid);
 };
 
 // Temporary :)

diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp
index 3656982..edb32c3 100644 (file)
--- a/src/mc/mc_base.cpp
+++ b/src/mc/mc_base.cpp
@@ -15,6 +15,7 @@
 
 #if SIMGRID_HAVE_MC
 #include "src/mc/ModelChecker.hpp"
+#include "src/mc/Session.hpp"
 #include "src/mc/remote/RemoteClient.hpp"
 
 using simgrid::mc::remote;
@@ -72,7 +73,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 mc_model_checker->process().actor_is_enabled(actor->get_pid());
+    return simgrid::mc::session->actor_is_enabled(actor->get_pid());
   }
 #endif
 

diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index b6732f6..73721ca 100644 (file)
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -7,7 +7,10 @@
 #include <signal.h>
 #include <sys/wait.h>
 
-simgrid::mc::CheckerSide::~CheckerSide()
+namespace simgrid {
+namespace mc {
+
+CheckerSide::~CheckerSide()
 {
   if (socket_event_ != nullptr)
     event_free(socket_event_);
@@ -17,7 +20,7 @@ simgrid::mc::CheckerSide::~CheckerSide()
     event_base_free(base_);
 }
 
-void simgrid::mc::CheckerSide::start(int socket, void (*handler)(int, short, void*))
+void CheckerSide::start(int socket, void (*handler)(int, short, void*))
 {
   base_ = event_base_new();
 
@@ -28,12 +31,15 @@ void simgrid::mc::CheckerSide::start(int socket, void (*handler)(int, short, voi
   event_add(signal_event_, NULL);
 }
 
-void simgrid::mc::CheckerSide::dispatch()
+void CheckerSide::dispatch()
 {
   event_base_dispatch(base_);
 }
 
-void simgrid::mc::CheckerSide::break_loop()
+void CheckerSide::break_loop()
 {
   event_base_loopbreak(base_);
 }
+
+} // namespace mc
+} // namespace simgrid

diff --git a/src/mc/remote/RemoteClient.cpp b/src/mc/remote/RemoteClient.cpp
index 08ed484..25bd083 100644 (file)
--- a/src/mc/remote/RemoteClient.cpp
+++ b/src/mc/remote/RemoteClient.cpp
@@ -625,15 +625,5 @@ void RemoteClient::dump_stack()
   _UPT_destroy(context);
   unw_destroy_addr_space(as);
 }
-
-bool RemoteClient::actor_is_enabled(aid_t pid)
-{
-  s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
-  process()->get_channel().send(msg);
-  char buff[MC_MESSAGE_LENGTH];
-  ssize_t received = process()->get_channel().receive(buff, MC_MESSAGE_LENGTH, true);
-  xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED");
-  return ((s_mc_message_int_t*)buff)->value;
-}
 }
 }

diff --git a/src/mc/remote/RemoteClient.hpp b/src/mc/remote/RemoteClient.hpp
index 87c5c7a..829d0ee 100644 (file)
--- a/src/mc/remote/RemoteClient.hpp
+++ b/src/mc/remote/RemoteClient.hpp
@@ -272,9 +272,6 @@ public:
   /** The corresponding context
    */
   void* unw_underlying_context;
-
-  /* Check whether the given actor is enabled */
-  bool actor_is_enabled(aid_t pid);
 };
 
 /** Open a FD to a remote process memory (`/dev/$pid/mem`)