[mc] Add methods to Session

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 7a28d28..698b546 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -26,6 +26,7 @@
 #include "src/mc/SafetyChecker.hpp"
 #include "src/mc/VisitedState.hpp"
 #include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
@@ -116,26 +117,20 @@ int SafetyChecker::run()
         continue;
     }
 
-    int req_num = state->transition.argument;
-
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
     XBT_DEBUG("Execute: %s",
       simgrid::mc::request_to_string(
-        req, req_num, simgrid::mc::RequestType::simix).c_str());
+        req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
 
     std::string req_str;
     if (dot_output != nullptr)
-      req_str = simgrid::mc::request_get_dot_output(req, req_num);
+      req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 
     mc_stats->executed_transitions++;
 
-    // TODO, bundle both operations in a single message
-    //   MC_execute_transition(req, req_num)
-
     /* Answer the request */
-    mc_model_checker->handle_simcall(state->transition);
-    mc_model_checker->wait_for_requests();
+    this->getSession().execute(state->transition);
 
     /* Create the new expanded state */
     std::unique_ptr<simgrid::mc::State> next_state =

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 63c0c74..842fa3c 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -94,6 +94,12 @@ Session::~Session()
   this->close();
 }
 
+void Session::execute(Transition const& transition)
+{
+  modelChecker_->handle_simcall(transition);
+  modelChecker_->wait_for_requests();
+}
+
 // static
 Session* Session::fork(std::function<void(void)> code)
 {

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 9b7d857..23e3eaa 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -49,6 +49,9 @@ public:
   ~Session();
   void close();
 
+public:
+  void execute(Transition const& transition);
+
 public: // static constructors
 
   /** Create a new session by forking