if(_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
if (pair->graph_state->system_state_) {
- pair->graph_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
+ mcapi::get().restore_state(pair->graph_state->system_state_);
return;
}
}
/* Restore the initial state */
- mc::session->restore_initial_state();
+ mcapi::get().restore_initial_state();
/* Traverse the stack from the initial state and re-execute the transitions */
int depth = 1;
/* 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().simcall_get_issuer(saved_req);
req = &issuer->simcall_;
/* Debug information */
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth,
mcapi::get().request_to_string(req, req_num, simgrid::mc::RequestType::simix).c_str(), state.get());
- this->get_session().execute(state->transition_);
+ mcapi::get().execute(state->transition_);
}
/* Update statistics */
visited_pairs_count_++;
- mc_model_checker->executed_transitions++;
+ mcapi::get().mc_inc_executed_trans();
depth++;
}
}
}
-LivenessChecker::LivenessChecker(Session& s) : Checker(s)
+LivenessChecker::LivenessChecker() : Checker()
{
}
Checker* createLivenessChecker(Session& s)
{
- return new LivenessChecker(s);
+ return new LivenessChecker();
}
} // namespace mc