void DFSExplorer::check_non_termination(const State* current_state)
{
- for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
- if (*(*state)->get_system_state() == *current_state->get_system_state()) {
- XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num());
+ for (auto const& state : stack_) {
+ if (*state->get_system_state() == *current_state->get_system_state()) {
+ XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
XBT_INFO("******************************************");
throw TerminationError();
}
+ }
}
RecordTrace DFSExplorer::get_record_trace() // override
continue;
}
- // Backtrack if we are revisiting a state we saw previously
+ // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction
if (visited_state_ != nullptr) {
XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
stack_.size() + 1);
if (state->get_actor_count() == 0) {
- mc_model_checker->finalize_app();
+ get_remote_app().finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- state->execute_next(next);
+ state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
/* Create the new expanded state (copy the state of MCed into our MCer data) */
std::unique_ptr<State> next_state;
- /* If we want sleep set reduction, pass the old state to the new state so it can
- * both copy the sleep set and eventually removes things from it locally */
- if (_sg_mc_sleep_set)
- next_state = std::make_unique<State>(get_remote_app(), state);
- else
- next_state = std::make_unique<State>(get_remote_app());
+ next_state = std::make_unique<State>(get_remote_app(), state);
on_state_creation_signal(next_state.get(), get_remote_app());
/* If asked to rollback on a state that has a snapshot, restore it */
State* last_state = stack_.back().get();
if (const auto* system_state = last_state->get_system_state()) {
- system_state->restore(&get_remote_app().get_remote_process());
+ system_state->restore(get_remote_app().get_remote_process_memory());
on_restore_system_state_signal(last_state, get_remote_app());
return;
}