}
}
XBT_INFO("Expanded states = %lu", expanded_states_count_);
- XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
- XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+ XBT_INFO("Visited states = %lu", mcapi::get().mc_get_visited_states());
+ XBT_INFO("Executed transitions = %lu", mcapi::get().mc_get_executed_trans());
XBT_INFO("Send-deterministic : %s", this->send_deterministic ? "Yes" : "No");
if (_sg_mc_comms_determinism)
XBT_INFO("Recv-deterministic : %s", this->recv_deterministic ? "Yes" : "No");
static inline bool all_communications_are_finished()
{
- for (size_t current_actor = 1; current_actor < mcapi::get().get_maxpid(); current_actor++) {
+ auto maxpid = mcapi::get().get_maxpid();
+ for (size_t current_actor = 1; current_actor < maxpid; current_actor++) {
if (not incomplete_communications_pattern[current_actor].empty()) {
XBT_DEBUG("Some communications are not finished, cannot stop the exploration! State not visited.");
return false;
}
/* Restore the initial state */
- mc::session->restore_initial_state();
+ mcapi::get().s_restore_initial_state();
- unsigned n = MC_smx_get_maxpid();
+ unsigned n = mcapi::get().get_maxpid();
assert(n == incomplete_communications_pattern.size());
assert(n == initial_communications_pattern.size());
for (unsigned j=0; j < n ; j++) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ const smx_actor_t issuer = mcapi::get().mc_smx_simcall_get_issuer(saved_req);
smx_simcall_t req = &issuer->simcall_;
/* TODO : handle test and testany simcalls */
e_mc_call_type_t call = MC_get_call_type(req);
- mc_model_checker->handle_simcall(state->transition_);
+ mcapi::get().handle_simcall(state->transition_);
MC_handle_comm_pattern(call, req, req_num, 1);
- mc_model_checker->wait_for_requests();
+ mcapi::get().mc_wait_for_requests();
/* Update statistics */
- mc_model_checker->visited_states++;
- mc_model_checker->executed_transitions++;
+ mcapi::get().mc_inc_visited_states();
+ mcapi::get().mc_inc_executed_trans();
}
}