[mc] Add methods to Session

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 7a28d281ebbf62e257b71bc952098648f125f354..698b5463273947b478bb66f3f7959688aefb8977 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 63c0c7483b3cfe527c02a02ba313c27ff4f0f7a4..842fa3c86a0c03a52b20c800fb0399b654d0ebcd 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 9b7d857c138e32fe809238d971c920acbc563fbb..23e3eaa6f2ea0151b582d5f590035f14245c3bc7 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