// tree and decided upon "happens-before" at that point for different
// executions :(
if (wakeup_tree_.empty()) {
- if (const aid_t next = std::get<0>(next_transition_guided()); next >= 0) {
+ strategy_->consider_best();
+ if (const aid_t next = std::get<0>(strategy_->next_transition()); next >= 0) {
wakeup_tree_.insert(prior, odpor::PartialExecution{strategy_->actors_to_run_.at(next).get_transition()});
}
}
*/
void remove_subtree_starting_with(aid_t p);
+ bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+
/**
* @brief
*/
// (rather than following the partial execution of a
// wakeup tree). This corresponds to lines 9 to 13 of
// the ODPOR pseudocode
+ //
+ // INVARIANT: The execution sequence should be consistent
+ // with the state when seeding the tree. If the sequence
+ // gets out of sync with the state, selection will not
+ // work as we intend
state->seed_wakeup_tree_if_needed(execution_seq_);
}
std::shared_ptr<State> DFSExplorer::best_opened_state()
{
+ if (reduction_mode_ == ReductionMode::odpor) {
+ const auto first =
+ std::find_if(stack_.rbegin(), stack_.rend(), [](const auto& state) { return !state->has_empty_tree(); });
+ return *first;
+ }
+
int best_prio = 0; // cache the value for the best priority found so far (initialized to silence gcc)
auto best = end(opened_states_); // iterator to the state to explore having the best priority
auto valid = begin(opened_states_); // iterator marking the limit between states still to explore, and already
return;
}
}
+ xbt_die("Insertion should always succeed with the root node (which contains no "
+ "prior execution). If we've reached this point, this implies either that "
+ "the wakeup tree traversal is broken or that computation of the shortest "
+ "sequence to insert into the tree is broken");
}
} // namespace simgrid::mc::odpor
\ No newline at end of file
public:
std::string to_string(bool verbose) const override;
RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
- bool depends(const Transition* other) const override { return aid_ == other->aid_; } // Independent with any other transition
+ bool depends(const Transition* other) const override
+ {
+ if (other->type_ < type_)
+ return other->depends(this);
+
+ return aid_ == other->aid_;
+ } // Independent with any other transition
};
} // namespace simgrid::mc