}
}
-Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
-{
- s_mc_message_simcall_execute_t m = {};
- m.type = MessageType::SIMCALL_EXECUTE;
- m.aid_ = aid;
- m.times_considered_ = times_considered;
- checker_side_.get_channel().send(m);
-
- this->remote_process_memory_->clear_cache();
- if (this->remote_process_memory_->running())
- checker_side_.dispatch(); // 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);
- xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
- xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
- "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
- to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
-
- if (new_transition) {
- std::stringstream stream(answer.buffer.data());
- return deserialize_transition(aid, times_considered, stream);
- } else
- return nullptr;
-}
-
} // namespace simgrid::mc
void start();
- /** Let the application take a transition. A new Transition is created iff the last parameter is true */
- Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
-
Exploration* get_exploration() const { return exploration_; }
void set_exploration(Exploration* exploration) { exploration_ = exploration; }
}
}
+Transition* RemoteApp::handle_simcall(aid_t aid, int times_considered, bool new_transition)
+{
+ s_mc_message_simcall_execute_t m = {};
+ m.type = MessageType::SIMCALL_EXECUTE;
+ m.aid_ = aid;
+ m.times_considered_ = times_considered;
+ model_checker_->get_channel().send(m);
+
+ get_remote_process_memory().clear_cache();
+ if (this->get_remote_process_memory().running())
+ model_checker_->channel_handle_events(); // The app may send messages while processing the transition
+
+ s_mc_message_simcall_execute_answer_t answer;
+ ssize_t s = model_checker_->get_channel().receive(answer);
+ xbt_assert(s != -1, "Could not receive message");
+ xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
+ xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
+ "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
+ to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
+
+ if (new_transition) {
+ std::stringstream stream(answer.buffer.data());
+ return deserialize_transition(aid, times_considered, stream);
+ } else
+ return nullptr;
+}
+
void RemoteApp::finalize_app(bool terminate_asap)
{
s_mc_message_int_t m = {};
/* Get the list of actors that are ready to run at that step. Usually shorter than maxpid */
void get_actors_status(std::map<aid_t, simgrid::mc::ActorState>& whereto) const;
+ /** Take a transition. A new Transition is created iff the last parameter is true */
+ Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
+
/* Get the memory of the remote process */
RemoteProcessMemory& get_remote_process_memory() { return model_checker_->get_remote_process_memory(); }
// 2. Execute the actor according to the preparation above
Transition::executed_transitions_++;
- auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true);
+ auto* just_executed =
+ mc_model_checker->get_exploration()->get_remote_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"
replayed_transitions_++;
#if SIMGRID_HAVE_MC
- mc_model_checker->handle_simcall(aid_, times_considered_, false);
+ 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();
#endif
}