+ * @precondition: This method assumes that events `e` and
+ * `e' := get_latest_event_handle()` are in a *reversible* race,
+ * as is explicitly the case in SDPOR
+ *
+ * @returns a set of actors not already contained in `backtrack_set`
+ * which serve as an initials to reverse the race between `e`
+ * and `e' := get_latest_event_handle()`; that is, an initial that is
+ * not already contained in the set `backtrack_set`.
+ */
+ std::unordered_set<aid_t> get_missing_source_set_actors_from(EventHandle e,
+ const std::unordered_set<aid_t>& backtrack_set) const;
+
+ /**
+ * @brief Computes the analogous lines from the SDPOR algorithm
+ * in the ODPOR algorithm, viz. the intersection of the sleep set
+ * and the set of weak initials with respect to the given pair
+ * of racing events
+ *
+ * This method computes lines 4-6 of the ODPOR pseudocode, viz.:
+ *
+ * 4 | let E' := pre(E, e)
+ * 5 | let v := notdep(e, E).e'^
+ * 6 | if sleep(E') ∩ WI_[E'](v) = empty then
+ * 7 | --> wut(E') := insert_[E'](v, wut(E'))
+ *
+ * The sequence `v` is computed and returned as needed, based on whether
+ * the check on line 6 passes.
+ *
+ * @precondition: This method assumes that events `e` and
+ * `e_prime` are in a *reversible* race, as is the case
+ * in ODPOR.
+ *
+ * @returns a partial execution `v := notdep(e, E)` (where `E` refers
+ * to this execution) that should be inserted into a wakeup tree with
+ * respect to this execution if `sleep(E') ∩ WI_[E'](v) = empty`, and
+ * `std::nullopt` otherwise
+ */
+ std::optional<PartialExecution> get_odpor_extension_from(EventHandle e, EventHandle e_prime,
+ const State& state_at_e) const;
+
+ /**
+ * @brief For a given sequence of actors `v` and a sequence of transitions `w`,
+ * computes the sequence, if any, that should be inserted as a child in wakeup tree for
+ * this execution
+ *
+ * Recall that the procedure for implementing the insertion
+ * is outlined in section 6.2 of Abdulla et al. 2017 as follows:
+ *
+ * | Let `v` be the smallest (w.r.t to "<") sequence in [the tree] B
+ * | such that `v ~_[E] w`. If `v` is a leaf node, the tree can be left
+ * | unmodified.
+ * |
+ * | Otherwise let `w'` be the shortest sequence such that `w [=_[E] v.w'`
+ * | and add `v.w'` as a new leaf, ordered after all already existing nodes
+ * | of the form `v.w''`
+ *
+ * The procedure for determining whether `v ~_[E] w` is given as Lemma 4.6 of
+ * Abdulla et al. 2017:
+ *
+ * | The relation `v ~_[E] w` holds if either
+ * | (1) v = <>, or
+ * | (2) v := p.v' and either
+ * | (a) p in I_[E](w) and `v' ~_[E.p] (w \ p)`
+ * | (b) E ⊢ p ◊ w and `v' ~_[E.p] w`
+ *
+ * This method computes the result `v.w'` as needed (viz. only if `v ~_[E] w`
+ * with respect to this execution `E`). The implementation takes advantage
+ * of the fact that determining whether `v ~_[E] w` yields "for free" the
+ * the shortest such `w'` we are looking for; if we ultimately determine
+ * that `v ~_[E] w`, the work we did to do so leaves us precisely with `w'`,
+ * so we can simply prepend `v` to it and call it a day
+ *
+ * @precondition: This method assumes that `E.v` is a valid execution, viz.
+ * that the events of `E` are sufficient to enabled `v_0` and that
+ * `v_0, ..., v_{i - 1}` are sufficient to enable `v_i`. This is the
+ * case when e.g. `v := notdep(e, E).p` for example in ODPOR
+ *
+ * @returns a partial execution `v.w'` that should be inserted
+ * as a child of a wakeup tree node representing the sequence `v`
+ * if `v ~_[E] w`, or `std::nullopt` if that relation does not hold
+ * between the two sequences `v` and `w`
+ */
+ std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) const;
+
+ /**
+ * @brief For a given sequence `w`, determines whether p in I_[E](w)