mc_model_checker->executed_transitions++;
- /* Actually answer the request: let the remote process do execute that request */
+ /* Actually answer the request: let execute the selected request (MCed does one step) */
this->getSession().execute(state->transition);
- /* Create the new expanded state */
+ /* Create the new expanded state (copy the state of MCed into our MCer data) */
std::unique_ptr<simgrid::mc::State> next_state =
std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
this->checkNonTermination(next_state.get());
/* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
- if (_sg_mc_visited == true)
+ if (_sg_mc_max_visited_states == true)
visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
/* If this is a new state (or if we don't care about state-equality reduction) */
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
smx_simcall_t req = &state->internal_req;
if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
- xbt_die("Mutex is currently not supported with DPOR, "
- "use --cfg=model-check/reduction:none");
+ xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
+
const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
simgrid::mc::State* prev_state = i->get();
state->num);
}
- if (!prev_state->processStates[issuer->pid].isDone())
+ if (!prev_state->actorStates[issuer->pid].isDone())
prev_state->interleave(issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
if (_sg_mc_termination)
XBT_INFO("Check non progressive cycles");
else
- XBT_INFO("Check a safety property");
+ XBT_INFO("Check a safety property. Reduction is: %s.",
+ (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
+ (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
simgrid::mc::session->initialize();
XBT_DEBUG("Starting the safety algorithm");