+ /**
+ * @brief Computes the backtrack set for this state
+ * according to its definition in Simgrid.
+ *
+ * The backtrack set as it appears in DPOR, SDPOR, and ODPOR
+ * in SimGrid consists of those actors marked as `todo`
+ * (i.e. those that have yet to be explored) as well as those
+ * marked `done` (i.e. those that have already been explored)
+ * since the pseudocode in none of the above algorithms explicitly
+ * removes elements from the backtrack set. DPOR makes use
+ * explicitly of the `done` set, but we again note that the
+ * backtrack set still contains processes added to the done set.
+ */
+ std::unordered_set<aid_t> get_backtrack_set() const;
+ std::unordered_set<aid_t> get_sleeping_actors() const;
+ std::unordered_set<aid_t> get_enabled_actors() const;
+ std::map<aid_t, std::shared_ptr<Transition>> const& get_sleep_set() const { return sleep_set_; }
+ void add_sleep_set(std::shared_ptr<Transition> t) { sleep_set_.insert_or_assign(t->aid_, std::move(t)); }
+ 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
+ * associated with this state, if such an actor exists and if
+ * the wakeup tree is already not empty
+ *
+ * @param prior The sequence of steps leading up to this state
+ * with respec to which the tree associated with this state should be
+ * a wakeup tree (wakeup trees are defined relative to an execution)
+ *
+ * @invariant: You should not manipulate a wakeup tree with respect
+ * to more than one execution; doing so will almost certainly lead to
+ * unexpected results as wakeup trees are defined relative to a single
+ * execution
+ */
+ void seed_wakeup_tree_if_needed(const odpor::Execution& prior);
+
+ /**
+ * @brief Initializes the wakeup_tree_ instance by taking the subtree rooted at the
+ * single-process node `N` running actor `p := "actor taken by parent to form this state"`
+ * of the *parent's* wakeup tree
+ */
+ void sprout_tree_from_parent_state();
+
+ /**
+ * @brief Removes the subtree rooted at the single-process node
+ * `N` running actor `p` of this state's wakeup tree
+ */
+ void remove_subtree_using_current_out_transition();
+ bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+
+ /**
+ * @brief
+ */
+ odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
+
+ /** @brief Prepares the state for re-exploration following
+ * another after having followed ODPOR from this state with
+ * the current out transition
+ *
+ * After ODPOR has completed searching a maximal trace, it
+ * finds the first point in the execution with a nonempty wakeup
+ * tree. This method corresponds to lines 20 and 21 in the ODPOR
+ * pseudocode
+ */
+ void do_odpor_unwind();
+