+
+std::unordered_set<aid_t> State::get_enabled_actors() const
+{
+ std::unordered_set<aid_t> actors;
+ for (const auto& [aid, state] : get_actors_list()) {
+ if (state.is_enabled()) {
+ actors.insert(aid);
+ }
+ }
+ return actors;
+}
+
+void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
+{
+ // TODO: It would be better not to have such a flag.
+ if (has_initialized_wakeup_tree) {
+ return;
+ }
+ // TODO: Note that the next action taken by the actor may be updated
+ // after it executes. But we will have already inserted it into the
+ // tree and decided upon "happens-before" at that point for different
+ // executions :(
+ if (wakeup_tree_.empty()) {
+ 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()});
+ }
+ }
+ has_initialized_wakeup_tree = true;
+}
+
+void State::sprout_tree_from_parent_state()
+{
+ xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
+ "(or what appears to be, rather for state without a parent defined)");
+ const auto p = parent_state_->get_transition_out()->aid_;
+ const auto branch = std::find_if(
+ parent_state_->wakeup_tree_.begin(), parent_state_->wakeup_tree_.end(),
+ [=](const odpor::WakeupTreeNode* node) { return node->is_single_process() && node->get_first_actor() == p; });
+ xbt_assert(branch != parent_state_->wakeup_tree_.end(),
+ "Attempted to create a subtree from the wakeup tree of the parent "
+ "state using actor `%ld`, but no such subtree could be found. "
+ "This implies that the wakeup tree management is broken, "
+ "and more specifically that subtree formation is not working "
+ "as intended; for if this state was generated by the parent "
+ "having taken an action by actor `%ld`, this implies that "
+ "ODPOR found `%ld` as a candidate branch prior",
+ p, p, p);
+ this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(*branch);
+}
+
+void State::remove_subtree_starting_with(aid_t p)
+{
+ const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) {
+ return node->is_single_process() && node->get_first_actor() == p;
+ });
+ xbt_assert(branch != wakeup_tree_.end(), "Attempted to remove a subtree of this state's "
+ "wakeup tree that does not exist");
+ this->wakeup_tree_.remove_subtree_rooted_at(*branch);
+}
+
+void State::mark_path_interesting_for_odpor(const odpor::PartialExecution& pe, const odpor::Execution& E)
+{
+ this->wakeup_tree_.insert(E, pe);
+}
+