return process_info;
}
-bool Api::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
- RemotePtr<kernel::actor::SimcallObserver> obs2) const
-{
- xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
- return mc_model_checker->requests_are_dependent(obs1, obs2);
-}
-
xbt::string const& Api::get_actor_host_name(smx_actor_t actor) const
{
if (mc_model_checker == nullptr)
mc_model_checker->visited_states++;
}
-void Api::mc_inc_executed_trans() const
-{
- mc_model_checker->executed_transitions++;
-}
-
unsigned long Api::mc_get_visited_states() const
{
return mc_model_checker->visited_states;
}
-unsigned long Api::mc_get_executed_trans() const
-{
- return mc_model_checker->executed_transitions;
-}
-
void Api::mc_check_deadlock() const
{
if (mc_model_checker->checkDeadlock()) {
XBT_CINFO(mc_global, "Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
XBT_CINFO(mc_global, " %s", s.c_str());
- simgrid::mc::dumpRecordPath();
+ XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
simgrid::mc::session_singleton->log_state();
throw DeadlockError();
}
THROW_IMPOSSIBLE;
}
-void Api::handle_simcall(Transition const& transition) const
-{
- mc_model_checker->handle_simcall(transition);
-}
-
-void Api::mc_wait_for_requests() const
-{
- mc_model_checker->wait_for_requests();
-}
-
void Api::mc_exit(int status) const
{
mc_model_checker->exit(status);
}
-void Api::dump_record_path() const
-{
- simgrid::mc::dumpRecordPath();
-}
-
-/* Search for an enabled transition amongst actors
- *
- * This is the first actor marked TODO by the checker, and currently enabled in the application.
- *
- * Once we found it, prepare its execution (increase the times_considered of its observer and remove it as done on need)
- *
- * If we can't find any actor, return false
- */
-
-bool Api::mc_state_choose_request(simgrid::mc::State* state) const
-{
- RemoteProcess& process = mc_model_checker->get_remote_process();
- XBT_DEBUG("Search for an actor to run. %zu actors to consider", process.actors().size());
- for (auto& actor_info : process.actors()) {
- auto actor = actor_info.copy.get_buffer();
- simgrid::mc::ActorState* actor_state = &state->actor_states_[actor->get_pid()];
-
- /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/
- if (not actor_state->is_todo() || not simgrid::mc::actor_is_enabled(actor))
- continue;
-
- /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */
- if (actor->simcall_.observer_ != nullptr) {
- state->transition_.times_considered_ = actor_state->get_times_considered_and_inc();
- if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered())
- actor_state->set_done();
- } else {
- state->transition_.times_considered_ = 0;
- actor_state->set_done();
- }
-
- state->transition_.aid_ = actor->get_pid();
- state->executed_req_ = actor->simcall_;
-
- XBT_DEBUG("Let's run actor %ld, going for transition %s", actor->get_pid(),
- SIMIX_simcall_name(state->executed_req_));
- return true;
- }
- return false;
-}
-
-std::string Api::request_get_dot_output(aid_t aid, int value) const
+std::string Api::request_get_dot_output(const Transition* t) const
{
- const char* color = get_color(aid - 1);
- return "label = \"" + mc_model_checker->simcall_dot_label(aid, value) + "\", color = " + color +
- ", fontcolor = " + color;
+ const char* color = get_color(t->aid_ - 1);
+ return "label = \"" + t->dot_label() + "\", color = " + color + ", fontcolor = " + color;
}
#if HAVE_SMPI
return simgrid::mc::snapshot_equal(s1, s2);
}
-simgrid::mc::Snapshot* Api::take_snapshot(int num_state) const
+simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
{
auto snapshot = new simgrid::mc::Snapshot(num_state);
return snapshot;
void Api::automaton_load(const char* file) const
{
- MC_automaton_load(file);
+ if (simgrid::mc::property_automaton == nullptr)
+ simgrid::mc::property_automaton = xbt_automaton_new();
+
+ xbt_automaton_load(simgrid::mc::property_automaton, file);
}
std::vector<int> Api::automaton_propositional_symbol_evaluate() const