MC: move the reversible_race logic to the Transition class

[simgrid.git] / src / mc / explo / odpor / Execution.cpp

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 8b531ff..0694161 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -5,7 +5,6 @@
 
 #include "src/mc/explo/odpor/Execution.hpp"
 #include "src/mc/api/State.hpp"
-#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
 #include "xbt/asserts.h"
 #include "xbt/string.hpp"
 #include <algorithm>
@@ -106,9 +105,7 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
     // it (since this would transitively make it the event
     // which "happens-between" `target` and `e`)
     if (disqualified_events.count(e_i) == 0) {
-       XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event",
-                  target, e_i);
-        disqualified_events.insert(e_i);
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", target, e_i);
       racing_events.insert(e_i);
       disqualified_events.insert(e_i);
     }
@@ -120,8 +117,11 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
 std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
 {
   std::unordered_set<EventHandle> reversible_races;
+  const auto* this_transition = get_transition_for_handle(handle);
   for (EventHandle race : get_racing_events_of(handle)) {
-    if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) {
+    const auto* other_transition = get_transition_for_handle(race);
+
+    if (this_transition->reversible_race(other_transition)) {
       reversible_races.insert(race);
     }
   }
@@ -280,6 +280,9 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
       E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
       v.push_back(get_event_with_handle(e_star).get_transition());
 
+      XBT_DEBUG("Added Event `%u` (%ld:%s) to the construction of v", e_star, get_actor_with_handle(e_star),
+                get_event_with_handle(e_star).get_transition()->to_string().c_str());
+
       const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
 
       // When checking whether any event in `dom_[E'](v)` happens before
@@ -317,6 +320,9 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
         // relation orders actions taken by each actor
         disqualified_actors.insert(q);
       }
+    } else {
+      XBT_DEBUG("Event `%u` (%ld:%s) dismissed from the construction of v", e_star, get_actor_with_handle(e_star),
+                get_event_with_handle(e_star).get_transition()->to_string().c_str());
     }
   }