X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2938350ef873d235860bee051062edcfd2596da6..7e625e5e848a284b522d69ec28cb111f1f88515b:/src/mc/explo/odpor/Execution.cpp

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index 5c9d72bf2f..0694161cd2 100644
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -5,13 +5,14 @@
 
 #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>
 #include <limits>
 #include <vector>
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
 namespace simgrid::mc::odpor {
 
 std::vector<std::string> get_textual_trace(const PartialExecution& w)
@@ -64,18 +65,22 @@ std::vector<std::string> Execution::get_textual_trace() const
 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;
+  // This keep tracks of events that happens-before the target
   std::unordered_set<Execution::EventHandle> disqualified_events;
 
   // For each event of the execution
   for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
     // We need `e_i -->_E target` as a necessary condition
     if (not happens_before(e_i, target)) {
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target);
       continue;
     }
 
     // Further, `proc(e_i) != proc(target)`
     if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
       disqualified_events.insert(e_i);
+      XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i,
+                target);
       continue;
     }
 
@@ -87,6 +92,8 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
       // then e_i --->_E target indirectly (either through
       // e_j directly, or transitively through e_j)
       if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
+        XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)",
+                  target, e_i, e_j, e_i, e_j, target);
         disqualified_events.insert(e_i);
         break;
       }
@@ -98,6 +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);
       racing_events.insert(e_i);
       disqualified_events.insert(e_i);
     }
@@ -109,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);
     }
   }
@@ -269,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
@@ -287,8 +301,8 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
       if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial?
         continue;
       }
-      const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
-        return E_prime_v.happens_before(e_star, e_star_in_E_prime_v);
+      const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+        return E_prime_v.happens_before(handle, e_star_in_E_prime_v);
       });
       if (is_initial) {
         // If the sleep set already contains `q`, we're done:
@@ -306,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());
     }
   }
 
@@ -320,8 +337,8 @@ std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle
   const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
   v_handles.push_back(e_prime_in_E_prime_v);
 
-  const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
-    return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
+  const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+    return E_prime_v.happens_before(handle, e_prime_in_E_prime_v);
   });
   if (is_initial) {
     if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {