+ } else if (reduction_mode_ == ReductionMode::sdpor) {
+ /**
+ * SDPOR Source Set Procedure:
+ *
+ * Find "reversible races" in the current execution `E` with respect
+ * to the latest action `p`. For each such race, determine one thread
+ * not contained in the backtrack set at the "race point" `r` which
+ * "represents" the trace formed by first executing everything after
+ * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
+ * flip the race.
+ *
+ * The intuition is that some subsequence of `v` may enable `p`, so
+ * we want to be sure that search "in that direction"
+ */
+ execution_seq_.push_transition(std::move(executed_transition));
+ xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
+ "No events are contained in the SDPOR/OPDPOR execution "
+ "even though one was just added");
+
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+ for (const auto racing_event_handle : execution_seq_.get_reversible_races_of(next_E_p)) {
+ const std::shared_ptr<State> prev_state = stack_[racing_event_handle];
+ // NOTE: To incorporate the idea of attempting to select the "best"
+ // backtrack point into SDPOR, instead of selecting the `first` initial,
+ // we should instead compute all choices and decide which is best
+ if (const auto q =
+ execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
+ q.has_value()) {
+ prev_state->consider_one(q.value());
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ }
+ } else if (reduction_mode_ == ReductionMode::odpor) {
+ // In the case of ODPOR, we simply observe the transition that was executed
+ // until we've reached a maximal trace
+ execution_seq_.push_transition(std::move(executed_transition));