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:
// 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"
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
/* 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;
}
/* 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
}
}
- 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 */
"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)