From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Wed, 8 Nov 2023 15:44:10 +0000 (+0100)
Subject: Fix ODPOR: overapproximate ReversibleRace (to not miss branches) and survive overapprox
X-Git-Tag: v3.35~86^2
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3e9e2c3010b77637029ad9d6503de5ddccb38daa

Fix ODPOR: overapproximate ReversibleRace (to not miss branches) and survive overapprox

Optimal DPOR just became sub-optimal :)
---

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 978cdfd1ef..0fb95fd182 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -136,7 +136,9 @@ void DFSExplorer::run()
     const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
                                                                : std::get<0>(state->next_transition_guided());
 
-    if (next < 0) { // If there is no more transition in the current state, backtrack.
+    if (next < 0 || not state->is_actor_enabled(next)) {
+      // If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
+      // ReversibleRace is an overapproximation), backtrace
       XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
                stack_.size() + 1);
 
diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index d671e93703..f449d6a363 100644
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -199,7 +199,7 @@ bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Exec
 {
   // TODO: We need to check if any of the transitions
   // waited on occurred before `e1`
-  return false;
+  return true; // Let's overapproximate to not miss branches
 }
 
 } // namespace simgrid::mc::odpor