Set the textual representation of a transition before executing it

This way it will correctly be set if the App aborts or fails during that execution.

Also, don't use the execution path that is reserved to simcalls with
observers `mc_model_checker->simcall_to_string()` in any case.
Prefer the path that works with old simcalls too `Api::request_to_string()`

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 1bdd4a1..a7847e7 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -1049,11 +1049,14 @@ void Api::restore_initial_state() const
   session->restore_initial_state();
 }
 
-void Api::execute(Transition const& transition) const
+void Api::execute(Transition& transition, smx_simcall_t simcall) const
 {
-  session->execute(transition);
-  auto textual = mc_model_checker->simcall_to_string(transition.pid_, transition.times_considered_);
+  /* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
+  auto textual =
+      simgrid::mc::Api::get().request_to_string(simcall, transition.times_considered_, RequestType::executed);
   strcpy((char*)transition.textual, textual.c_str());
+
+  session->execute(transition);
 }
 
 #if SIMGRID_HAVE_MC

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index b2a5e8c..2252349 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -136,7 +136,7 @@ public:
   // SESSION APIs
   void session_initialize() const;
   void s_close() const;
-  void execute(Transition const& transition) const;
+  void execute(Transition& transition, smx_simcall_t simcall) const;
 
 // AUTOMATION APIs
 #if SIMGRID_HAVE_MC

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 705ce85..41ddff8 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -143,7 +143,7 @@ void LivenessChecker::replay()
       XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
                 api::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
 
-      api::get().execute(state->transition_);
+      api::get().execute(state->transition_, req);
     }
 
     /* Update statistics */

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index c1d4620..6d06ac4 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -131,7 +131,7 @@ void SafetyChecker::run()
     api::get().mc_inc_executed_trans();
 
     /* Actually answer the request: let execute the selected request (MCed does one step) */
-    api::get().execute(state->transition_);
+    api::get().execute(state->transition_, &state->executed_req_);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     ++expanded_states_count_;
@@ -258,7 +258,7 @@ void SafetyChecker::restore_state()
   for (std::unique_ptr<State> const& state : stack_) {
     if (state == stack_.back())
       break;
-    api::get().execute(state->transition_);
+    api::get().execute(state->transition_, &state->executed_req_);
     /* Update statistics */
     api::get().mc_inc_visited_states();
     api::get().mc_inc_executed_trans();