From 239cd16f4e95031d3a106e487c1485726069f1d7 Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Fri, 17 Mar 2023 22:23:09 +0100
Subject: [PATCH] A few calls to mc_model_checker less by passing more
 parameters

---
 src/mc/api/State.cpp             | 7 +++----
 src/mc/api/State.hpp             | 5 +++--
 src/mc/explo/DFSExplorer.cpp     | 2 +-
 src/mc/explo/LivenessChecker.cpp | 2 +-
 src/mc/explo/UdporChecker.cpp    | 2 +-
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index e81998b678..90045f501b 100644
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -102,7 +102,7 @@ aid_t State::next_transition() const
   return -1;
 }
 
-void State::execute_next(aid_t next)
+void State::execute_next(aid_t next, RemoteApp& app)
 {
   // This actor is ready to be executed. Execution involves three phases:
 
@@ -118,8 +118,7 @@ void State::execute_next(aid_t next)
 
   // 2. Execute the actor according to the preparation above
   Transition::executed_transitions_++;
-  auto* just_executed =
-      mc_model_checker->get_exploration()->get_remote_app().handle_simcall(next, times_considered, true);
+  auto* just_executed = app.handle_simcall(next, times_considered, true);
   xbt_assert(just_executed->type_ == expected_executed_transition->type_,
              "The transition that was just executed by actor %ld, viz:\n"
              "%s\n"
@@ -138,6 +137,6 @@ void State::execute_next(aid_t next)
   auto executed_transition = std::unique_ptr<Transition>(just_executed);
   actor_state.set_transition(std::move(executed_transition), times_considered);
 
-  mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
+  app.wait_for_requests();
 }
 } // namespace simgrid::mc
diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 06c6c5680f..2f4407fb3a 100644
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -57,8 +57,9 @@ public:
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   aid_t next_transition() const;
 
-  /* Explore a new path; the parameter must be the result of a previous call to next_transition() */
-  void execute_next(aid_t next);
+  /* Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
+   * next_transition() */
+  void execute_next(aid_t next, RemoteApp& app);
 
   long get_num() const { return num_; }
   std::size_t count_todo() const;
diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 761e13637b..84753958e4 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -152,7 +152,7 @@ void DFSExplorer::run()
     }
 
     /* Actually answer the request: let's execute the selected request (MCed does one step) */
-    state->execute_next(next);
+    state->execute_next(next, get_remote_app());
     on_transition_execute_signal(state->get_transition(), get_remote_app());
 
     // If there are processes to interleave and the maximum depth has not been
diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 4a61c0746b..370a146d0b 100644
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -399,7 +399,7 @@ void LivenessChecker::run()
       }
     }
 
-    current_pair->app_state_->execute_next(current_pair->app_state_->next_transition());
+    current_pair->app_state_->execute_next(current_pair->app_state_->next_transition(), get_remote_app());
     XBT_DEBUG("Execute: %s", current_pair->app_state_->get_transition()->to_string().c_str());
 
     /* Update the dot output */
diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 4d89514798..4863807268 100644
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -194,7 +194,7 @@ void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
                               "one transition of the state of an visited event is enabled, yet no\n"
                               "state was actually enabled. Please report this as a bug.\n"
                               "*********************************\n\n");
-  state.execute_next(next_actor);
+  state.execute_next(next_actor, get_remote_app());
 }
 
 void UdporChecker::restore_program_state_to(const State& stateC)
-- 
2.20.1