- if (prev_state.is_actor_enabled(p)) {
- const std::optional<odpor::PartialExecution> v =
- execution_seq_.get_odpor_extension_from(e, e_prime, prev_state);
- if (v.has_value()) {
- prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(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());