/* Debug information */
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
- request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
+ mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
this->get_session().execute(state->transition_);
}
{
XBT_INFO("Expanded pairs = %lu", expanded_pairs_count_);
XBT_INFO("Visited pairs = %lu", visited_pairs_count_);
- XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+ XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans());
}
void LivenessChecker::show_acceptance_cycle(std::size_t depth)
XBT_INFO("Counter-example that violates formula:");
for (auto const& s : this->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- mc::dumpRecordPath();
- mc::session->log_state();
+ mcapi::get().dump_record_path();
+ mcapi::get().log_state();
XBT_INFO("Counter-example depth: %zu", depth);
}
int req_num = pair->graph_state->transition_.argument_;
smx_simcall_t req = &pair->graph_state->executed_req_;
if (req->call_ != simix::Simcall::NONE)
- trace.push_back(request_to_string(req, req_num, RequestType::executed));
+ trace.push_back(mcapi::get().request_to_string(req, req_num, RequestType::executed));
}
return trace;
}
void LivenessChecker::run()
{
XBT_INFO("Check the liveness property %s", _sg_mc_property_file.get().c_str());
- MC_automaton_load(_sg_mc_property_file.get().c_str());
+ mcapi::get().automaton_load(_sg_mc_property_file.get().c_str());
XBT_DEBUG("Starting the liveness algorithm");
- mc::session->initialize();
+ mcapi::get().session_initialize();
/* Initialize */
this->previous_pair_ = 0;
fflush(dot_output);
}
- XBT_DEBUG("Execute: %s", request_to_string(req, req_num, RequestType::simix).c_str());
+ XBT_DEBUG("Execute: %s", mcapi::get().request_to_string(req, req_num, RequestType::simix).c_str());
/* Update stats */
mc_model_checker->executed_transitions++;