A few calls to mc_model_checker less by passing more parameters

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index e81998b..90045f5 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -102,7 +102,7 @@ aid_t State::next_transition() const
   return -1;
 }
 
   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:
 
 {
   // 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_++;
 
   // 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"
   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);
 
   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
 }
 } // namespace simgrid::mc

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index 06c6c56..2f4407f 100644 (file)
--- 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;
 
   /* 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;
 
   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 761e136..8475395 100644 (file)
--- 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) */
     }
 
     /* 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
     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 4a61c07..370a146 100644 (file)
--- 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 */
     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 4d89514..4863807 100644 (file)
--- 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");
                               "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)
 }
 
 void UdporChecker::restore_program_state_to(const State& stateC)