Move request_execute and request_to_string from api::get() to Transition

diff --git a/src/mc/Transition.cpp b/src/mc/Transition.cpp
new file mode 100644 (file)
index 0000000..ba0337e
--- /dev/null
+++ b/src/mc/Transition.cpp
@@ -0,0 +1,26 @@
+/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved.          */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/Transition.hpp"
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/Session.hpp"
+#include "xbt/asserts.h"
+
+namespace simgrid {
+namespace mc {
+
+std::string Transition::to_string()
+{
+  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
+
+  return textual;
+}
+RemotePtr<simgrid::kernel::actor::SimcallObserver> Transition::execute()
+{
+  textual = mc_model_checker->simcall_to_string(aid_, times_considered_);
+  return session_singleton->execute(*this);
+}
+} // namespace mc
+} // namespace simgrid

diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp
index 33e9bba..64d097e 100644 (file)
--- a/src/mc/Transition.hpp
+++ b/src/mc/Transition.hpp
@@ -8,6 +8,7 @@
 #define SIMGRID_MC_TRANSITION_HPP
 
 #include "simgrid/forward.h" // aid_t
+#include "src/mc/remote/RemotePtr.hpp"
 #include <string>
 
 namespace simgrid {
@@ -37,6 +38,9 @@ public:
 
   /* Textual representation of the transition, to display backtraces */
   std::string textual = "";
+
+  std::string to_string();
+  RemotePtr<simgrid::kernel::actor::SimcallObserver> execute();
 };
 
 } // namespace mc

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 0a45d97..ab33c45 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -425,13 +425,6 @@ bool Api::mc_state_choose_request(simgrid::mc::State* state) const
   return false;
 }
 
-std::string Api::request_to_string(aid_t aid, int value) const
-{
-  xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
-  return mc_model_checker->simcall_to_string(aid, value);
-}
-
 std::string Api::request_get_dot_output(aid_t aid, int value) const
 {
   const char* color = get_color(aid - 1);
@@ -479,13 +472,6 @@ void Api::s_close() const
   session_singleton->close();
 }
 
-RemotePtr<simgrid::kernel::actor::SimcallObserver> Api::execute(Transition& transition) const
-{
-  /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
-  transition.textual = request_to_string(transition.aid_, transition.times_considered_);
-  return session_singleton->execute(transition);
-}
-
 void Api::automaton_load(const char* file) const
 {
   MC_automaton_load(file);

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index ed944ee..4a03606 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -109,7 +109,6 @@ public:
   // SIMCALL APIs
   bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
                               RemotePtr<kernel::actor::SimcallObserver> obs2) const;
-  std::string request_to_string(aid_t aid, int value) const;
   std::string request_get_dot_output(aid_t aid, int value) const;
   smx_actor_t simcall_get_issuer(s_smx_simcall const* req) const;
   RemotePtr<kernel::activity::MailboxImpl> get_mbox_remote_addr(smx_simcall_t const req) const;
@@ -129,7 +128,6 @@ public:
 
   // SESSION APIs
   void s_close() const;
-  RemotePtr<simgrid::kernel::actor::SimcallObserver> execute(Transition& transition) const;
 
 // AUTOMATION APIs
 #if SIMGRID_HAVE_MC

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index e402b1e..86ee54f 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -270,7 +270,7 @@ std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() //
 {
   std::vector<std::string> trace;
   for (auto const& state : stack_)
-    trace.push_back(api::get().request_to_string(state->transition_.aid_, state->transition_.times_considered_));
+    trace.push_back(state->transition_.to_string());
   return trace;
 }
 
@@ -429,7 +429,7 @@ void CommunicationDeterminismChecker::real_run()
       int req_num = cur_state->transition_.times_considered_;
       smx_simcall_t req = &cur_state->executed_req_;
 
-      XBT_DEBUG("Execute: %s", api::get().request_to_string(aid, req_num).c_str());
+      XBT_DEBUG("Execute: %s", cur_state->transition_.to_string().c_str());
 
       std::string req_str;
       if (dot_output != nullptr)

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index c11d63a..89dd0ab 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -122,12 +122,8 @@ void LivenessChecker::replay()
     std::shared_ptr<State> state = pair->graph_state;
 
     if (pair->exploration_started) {
-      /* Debug information */
-      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
-                api::get().request_to_string(state->transition_.aid_, state->transition_.times_considered_).c_str(),
-                state.get());
-
-      api::get().execute(state->transition_);
+      state->transition_.execute();
+      XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->transition_.to_string().c_str(), state.get());
     }
 
     /* Update statistics */
@@ -223,8 +219,7 @@ std::vector<std::string> LivenessChecker::get_textual_trace() // override
   for (std::shared_ptr<Pair> const& pair : exploration_stack_) {
     smx_simcall_t req = &pair->graph_state->executed_req_;
     if (req->call_ != simix::Simcall::NONE)
-      trace.push_back(api::get().request_to_string(pair->graph_state->transition_.aid_,
-                                                   pair->graph_state->transition_.times_considered_));
+      trace.push_back(pair->graph_state->transition_.to_string());
   }
   return trace;
 }
@@ -360,7 +355,7 @@ void LivenessChecker::run()
       fflush(dot_output);
     }
 
-    XBT_DEBUG("Execute: %s", api::get().request_to_string(aid, req_num).c_str());
+    XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str());
 
     /* Update stats */
     api::get().mc_inc_executed_trans();

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 8b8dcb8..fbaa3ac 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -124,11 +124,11 @@ void SafetyChecker::run()
     }
 
     /* Actually answer the request: let execute the selected request (MCed does one step) */
-    auto remote_observer = api::get().execute(state->transition_);
+    auto remote_observer = state->transition_.execute();
 
     // 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", state->transition_.textual.c_str());
+    XBT_DEBUG("Execute: %s", state->transition_.to_string().c_str());
 
     std::string req_str;
     if (dot_output != nullptr)
@@ -248,7 +248,7 @@ void SafetyChecker::restore_state()
   for (std::unique_ptr<State> const& state : stack_) {
     if (state == stack_.back())
       break;
-    api::get().execute(state->transition_);
+    state->transition_.execute();
     /* Update statistics */
     api::get().mc_inc_visited_states();
     api::get().mc_inc_executed_trans();

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 25b186b..db341ce 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -628,6 +628,7 @@ set(MC_SRC
   src/mc/mc_client_api.cpp
   src/mc/mc_smx.cpp
   src/mc/mc_exit.hpp
+  src/mc/Transition.cpp
   src/mc/Transition.hpp
   src/mc/udpor_global.cpp
   src/mc/udpor_global.hpp