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

diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h
index 96bcd6e..dae9277 100644 (file)
--- 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 969e5c3..6c109d4 100644 (file)
--- 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 edf1316..13488a0 100644 (file)
--- 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 bd33237..60857d8 100644 (file)
--- 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 0b735e8..9091592 100644 (file)
--- 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 fced9be..81b4f9a 100644 (file)
--- 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 1b6f8c3..70d94bb 100644 (file)
--- 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 64175c1..17fb7e6 100644 (file)
--- 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; }