This commit fixes the following two bugs:
1. When seeding a wakeup tree for the first
time, we forgot to add a `break` statement
to ensure that only one such enabled thread
were placed into the wakeup tree. Before
all such enabled threads were inserted which
amounted to what would have been a brute-force
search :(.
2. When determining whether a sequence is a
candidate for insertion into a wakeup tree,
we may need to check, for all enabled actors
in a given state, whether those actors'
next steps are independent with the sequence
theretofore constructed. This additional
step peforms the work needed to check whether
those actors are contained in the set of
*weak* initials. The method corresponds
to line 6 of the pseudocode of the ODPOR algorithm
for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
}
for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
}
+ break; // Only one actor gets inserted (see pseudocode)
"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");
"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");
-
- // TODO: This assert should even be bolstered to check that the
- // the transitions themselves are identical -- not only just
- // that the actors are the same. When we have to consider
- // multiple paths for a transition, things get trickier
- xbt_assert(parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor(),
- "We tried to make a subtree from a parent state who claimed to have executed %ld "
- "but whose wakeup tree indicates it should have executed %ld. This indicates "
+ xbt_assert((parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor()) &&
+ (parent_state_->get_transition_out()->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?",
"that exploration is not following ODPOR. Are you sure you're choosing actors "
"to schedule from the wakeup tree?",
- parent_state_->get_transition_out()->aid_, min_process_node.value()->get_actor());
+ parent_state_->get_transition_out()->to_string(false).c_str(),
+ min_process_node.value()->get_action()->to_string(false).c_str());
this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
}
void State::remove_subtree_using_current_out_transition()
{
if (auto out_transition = get_transition_out(); out_transition != nullptr) {
this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
}
void State::remove_subtree_using_current_out_transition()
{
if (auto out_transition = get_transition_out(); out_transition != nullptr) {
- // TODO: Add invariant check here
+ if (const auto min_process_node = wakeup_tree_.get_min_single_process_node(); min_process_node.has_value()) {
+ xbt_assert((out_transition->aid_ == min_process_node.value()->get_actor()) &&
+ (out_transition->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?",
+ out_transition->to_string(false).c_str(),
+ min_process_node.value()->get_action()->to_string(false).c_str());
+ }
wakeup_tree_.remove_min_single_process_subtree();
}
wakeup_tree_.remove_min_single_process_subtree();
}
{
sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
}
{
sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
}
+ bool is_actor_sleeping(aid_t actor) const
+ {
+ return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
+ sleep_set_.end();
+ }
/**
* @brief Inserts an arbitrary enabled actor into the wakeup tree
/**
* @brief Inserts an arbitrary enabled actor into the wakeup tree
// in case we want to consider multiple states (eg. during backtrack)
const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
: std::get<0>(state->next_transition_guided());
// in case we want to consider multiple states (eg. during backtrack)
const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
: std::get<0>(state->next_transition_guided());
+ xbt_assert(!state->is_actor_sleeping(next),
+ "We decided to schedule an actor (%ld) that is in the sleep set "
+ "of the current state. By definition, this should be impossible; "
+ "and yet it happened, somehow...",
+ next);
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
- if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
+ if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
disqualified_events.insert(e_i);
break;
}
disqualified_events.insert(e_i);
break;
}
for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
// TODO: We have to be able to react appropriately here when adding new
// types of transitions (multiple choices can be made :( )
for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
// TODO: We have to be able to react appropriately here when adding new
// types of transitions (multiple choices can be made :( )
- if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
+ if (astate.is_enabled() and sleeping_actors.count(aid) == 0 and
+ pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {