From 32b33834115ef974885e0227b9f47a1e756ee04c Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Sun, 19 Mar 2023 09:52:48 +0100
Subject: [PATCH] another mc_model_checker call location disappears

I postponned this one a lot because it's impacting non-MC code, but at
the end it went smoothly
---
 include/simgrid/forward.h        | 1 +
 src/mc/api/RemoteApp.cpp         | 4 ++--
 src/mc/explo/DFSExplorer.cpp     | 2 +-
 src/mc/explo/LivenessChecker.cpp | 2 +-
 src/mc/remote/CheckerSide.cpp    | 2 +-
 src/mc/remote/CheckerSide.hpp    | 2 +-
 src/mc/transition/Transition.cpp | 6 +++---
 src/mc/transition/Transition.hpp | 2 +-
 8 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h
index 96bcd6ed19..dae9277459 100644
--- a/include/simgrid/forward.h
+++ b/include/simgrid/forward.h
@@ -209,6 +209,7 @@ class Profile;
 } // namespace kernel
 namespace mc {
 class State;
+class RemoteApp;
 }
 } // namespace simgrid
 
diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 969e5c3d85..6c109d4197 100644
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -301,7 +301,7 @@ void RemoteApp::wait_for_requests()
   get_remote_process_memory().clear_cache();
 
   if (this->get_remote_process_memory().running())
-    checker_side_->dispatch();
+    checker_side_->dispatch_events();
 }
 
 void RemoteApp::shutdown()
@@ -327,7 +327,7 @@ Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_
 
   get_remote_process_memory().clear_cache();
   if (this->get_remote_process_memory().running())
-    checker_side_->dispatch(); // The app may send messages while processing the transition
+    checker_side_->dispatch_events(); // The app may send messages while processing the transition
 
   s_mc_message_simcall_execute_answer_t answer;
   ssize_t s = checker_side_->get_channel().receive(answer);
diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index edf1316724..13488a08c7 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -289,7 +289,7 @@ void DFSExplorer::backtrack()
     for (std::unique_ptr<State> const& state : stack_) {
       if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
         break;
-      state->get_transition()->replay();
+      state->get_transition()->replay(get_remote_app());
       on_transition_replay_signal(state->get_transition(), get_remote_app());
       visited_states_count_++;
     }
diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index bd332375fb..60857d84a6 100644
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -119,7 +119,7 @@ void LivenessChecker::replay()
     std::shared_ptr<State> state = pair->app_state_;
 
     if (pair->exploration_started) {
-      state->get_transition()->replay();
+      state->get_transition()->replay(get_remote_app());
       XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
     }
 
diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp
index 0b735e8af5..909159233a 100644
--- a/src/mc/remote/CheckerSide.cpp
+++ b/src/mc/remote/CheckerSide.cpp
@@ -59,7 +59,7 @@ CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
   signal_event_.reset(signal_event);
 }
 
-void CheckerSide::dispatch() const
+void CheckerSide::dispatch_events() const
 {
   event_base_dispatch(base_.get());
 }
diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp
index fced9be1e7..81b4f9aee8 100644
--- a/src/mc/remote/CheckerSide.hpp
+++ b/src/mc/remote/CheckerSide.hpp
@@ -33,7 +33,7 @@ public:
   Channel const& get_channel() const { return channel_; }
   Channel& get_channel() { return channel_; }
 
-  void dispatch() const;
+  void dispatch_events() const;
   void break_loop() const;
 };
 
diff --git a/src/mc/transition/Transition.cpp b/src/mc/transition/Transition.cpp
index 1b6f8c3ffa..70d94bb02f 100644
--- a/src/mc/transition/Transition.cpp
+++ b/src/mc/transition/Transition.cpp
@@ -45,13 +45,13 @@ std::string Transition::dot_string() const
   return xbt::string_printf("label = \"[(%ld)] %s\", color = %s, fontcolor = %s", aid_, Transition::to_c_str(type_),
                             color, color);
 }
-void Transition::replay() const
+void Transition::replay(RemoteApp& app) const
 {
   replayed_transitions_++;
 
 #if SIMGRID_HAVE_MC
-  mc_model_checker->get_exploration()->get_remote_app().handle_simcall(aid_, times_considered_, false);
-  mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
+  app.handle_simcall(aid_, times_considered_, false);
+  app.wait_for_requests();
 #endif
 }
 
diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp
index 64175c1932..17fb7e629f 100644
--- a/src/mc/transition/Transition.hpp
+++ b/src/mc/transition/Transition.hpp
@@ -66,7 +66,7 @@ public:
   virtual std::string dot_string() const;
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
-  void replay() const;
+  void replay(RemoteApp& app) const;
 
   virtual bool depends(const Transition* other) const { return true; }
 
-- 
2.20.1