+ if (const auto last_event = execution_seq_.get_latest_event_handle();
+ reduction_mode_ == ReductionMode::odpor and last_event.has_value()) {
+ /**
+ * ODPOR Race Detection Procedure:
+ *
+ * For each reversible race in the current execution, we note if there are any continuations `C` equivalent to that
+ * which would reverse the race that have already either a) been searched by ODPOR or b) been *noted* to be searched
+ * by the wakeup tree at the appropriate reversal point, either as `C` directly or an as equivalent to `C`
+ * ("eventually looks like C", viz. the `~_E` relation)
+ */
+ for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
+ for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+ XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
+ State& prev_state = *stack_[e];
+ if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
+ switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
+ case odpor::WakeupTree::InsertionResult::root: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::interior_node: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` partially accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::leaf: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ }
+ for (const auto& seq : simgrid::mc::odpor::get_textual_trace(v.value())) {
+ XBT_DEBUG(" %s", seq.c_str());
+ }
+ } else {
+ XBT_DEBUG("ODPOR: Ignoring race: `sleep(E')` intersects `WI_[E'](v := notdep(%u, E))`", e);
+ XBT_DEBUG("Sleep set contains:");
+ for (const auto& [aid, transition] : prev_state.get_sleep_set())
+ XBT_DEBUG(" <%ld,%s>", aid, transition->to_string().c_str());
+ }
+ }
+ }