From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Sun, 28 Feb 2021 23:38:00 +0000 (+0100)
Subject: Set the textual representation of a transition before executing it
X-Git-Tag: v3.27~307
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/975faee3cab10e7dadee66a29bbdb7bfaef6e05f

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 1bdd4a10c8..a7847e7334 100644
--- 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 b2a5e8c3ee..22523490a4 100644
--- 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 705ce853c8..41ddff8979 100644
--- 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 c1d4620027..6d06ac4601 100644
--- 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();