From: mlaurent <mathieu.laurent@ens-rennes.fr>
Date: Wed, 8 Nov 2023 17:56:03 +0000 (+0100)
Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid
X-Git-Tag: v3.35~86
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/861f43e45a240e3568c7db636d36d05ed3f70665?hp=eb115a05127cacf97d96dca1107ebfe60653e4bd

Merge branch 'master' of https://framagit.org/simgrid/simgrid
---

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 033c525924..d279303a5f 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 9b8f6144f0..7a944a4dd7 100644
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -213,7 +213,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