X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/861f43e45a240e3568c7db636d36d05ed3f70665..3f9b311ec56db95ec539001a860ae3c838c48312:/src/mc/explo/DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index d279303a5f..b328d15773 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -8,8 +8,10 @@
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
 #include "src/mc/mc_record.hpp"
+#include "src/mc/remote/mc_protocol.h"
 #include "src/mc/transition/Transition.hpp"
 
+#include "xbt/asserts.h"
 #include "xbt/log.h"
 #include "xbt/string.hpp"
 #include "xbt/sysdep.h"
@@ -137,6 +139,18 @@ void DFSExplorer::run()
                                                                : std::get<0>(state->next_transition_guided());
 
     if (next < 0 || not state->is_actor_enabled(next)) {
+      if (next >= 0) { // Actor is not enabled, then
+        XBT_DEBUG(
+            "Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
+            to_c_str(reduction_mode_), state->get_actors_list().at(next).get_transition()->to_string(true).c_str());
+        if (reduction_mode_ == ReductionMode::odpor) {
+          // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
+          state->remove_subtree_at_aid(next);
+          state->add_sleep_set(state->get_actors_list().at(next).get_transition());
+        } else {
+          xbt_assert(false, "Only ODPOR should be confident enought in itself to try executing a disabled transition");
+        }
+      }
       // 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(),
@@ -337,8 +351,6 @@ std::shared_ptr<State> DFSExplorer::next_odpor_state()
     for (const auto& [aid, transition] : state->get_sleep_set())
       XBT_DEBUG("\t  <%ld,%s>", aid, transition->to_string().c_str());
     if (not state->has_empty_tree()) {
-	XBT_DEBUG("\t    found the following non-empty WuT:\n"
-		  "%s", state->string_of_wut().c_str());
       return state;
     }
   }
@@ -358,8 +370,8 @@ void DFSExplorer::backtrack()
      * ("eventually looks like C", viz. the `~_E` relation)
      */
     for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
-	XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
-	for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+      XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
+      for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
         XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
         State& prev_state = *stack_[e];
         if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
@@ -421,7 +433,7 @@ void DFSExplorer::backtrack()
 
   // Search how to restore the backtracking point
   std::deque<Transition*> replay_recipe;
-  for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
+  for (const auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
     if (s->get_transition_in() != nullptr) // The root has no transition_in
       replay_recipe.push_front(s->get_transition_in().get());
   }