THROW_IMPOSSIBLE;
remote_app.get_actors_status(strategy_->actors_to_run_);
-
-#if SIMGRID_HAVE_STATEFUL_MC
- /* Stateful model checking */
- if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
- system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- *remote_app.get_remote_process_memory());
-#endif
}
State::State(RemoteApp& remote_app, std::shared_ptr<State> parent_state)
: incoming_transition_(parent_state->get_transition_out()), num_(++expended_states_), parent_state_(parent_state)
{
-
- if (_sg_mc_strategy == "none")
+ if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
else if (_sg_mc_strategy == "max_match_comm")
strategy_ = std::make_shared<MaxMatchComm>();
remote_app.get_actors_status(strategy_->actors_to_run_);
-#if SIMGRID_HAVE_STATEFUL_MC /* Stateful model checking */
- if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
- system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- *remote_app.get_remote_process_memory());
-#endif
-
/* Copy the sleep set and eventually removes things from it: */
/* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
* And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
{
std::unordered_set<aid_t> actors;
for (const auto& [aid, state] : get_actors_list()) {
- if (state.is_todo() or state.is_done()) {
+ if (state.is_todo() || state.is_done()) {
actors.insert(aid);
}
}
"parent with an empty wakeup tree. This indicates either that ODPOR "
"actor selection in State.cpp is incorrect, or that the code "
"deciding when to make subtrees in ODPOR is incorrect");
- xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) &&
- (get_transition_in()->type_ == min_process_node.value()->get_action()->type_),
- "We tried to make a subtree from a parent state who claimed to have executed `%s` "
- "but whose wakeup tree indicates it should have executed `%s`. This indicates "
- "that exploration is not following ODPOR. Are you sure you're choosing actors "
- "to schedule from the wakeup tree?",
- get_transition_in()->to_string(false).c_str(),
- min_process_node.value()->get_action()->to_string(false).c_str());
+ if (not(get_transition_in()->aid_ == min_process_node.value()->get_actor() &&
+ get_transition_in()->type_ == min_process_node.value()->get_action()->type_)) {
+ XBT_ERROR("We tried to make a subtree from a parent state who claimed to have executed `%s` on actor %ld "
+ "but whose wakeup tree indicates it should have executed `%s` on actor %ld. This indicates "
+ "that exploration is not following ODPOR. Are you sure you're choosing actors "
+ "to schedule from the wakeup tree? Trace so far:",
+ get_transition_in()->to_string(false).c_str(), get_transition_in()->aid_,
+ min_process_node.value()->get_action()->to_string(false).c_str(), min_process_node.value()->get_actor());
+ for (auto elm : Exploration::get_instance()->get_textual_trace())
+ XBT_ERROR("%s", elm.c_str());
+ xbt_abort();
+ }
this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
}
// works with ODPOR in the way we intend it to work. There is not a
// good way to perform transition equality in SimGrid; instead, we
// effectively simply check for the presence of an actor in the sleep set.
- if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+ if (not get_actors_list().at(out_transition->aid_).has_more_to_consider())
add_sleep_set(std::move(out_transition));
}
}