X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/59054b2bcebd6cdc83ca72089f320f244e3b9b4f..9fc682676a33abb6a4cc527c09a34db3c33e5711:/src/mc/explo/DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 978cdfd1ef..8d85325ef7 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"
@@ -81,7 +83,7 @@ void DFSExplorer::log_state() // override
   XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
            "visited overall)",
            State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
-	   visited_states_count_);
+           visited_states_count_);
   Exploration::log_state();
 }
 
@@ -136,7 +138,23 @@ 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 (next >= 0) { // Actor is not enabled, then
+        XBT_INFO("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) {
+          XBT_INFO("Current trace:");
+          for (auto elm : get_textual_trace())
+            XBT_ERROR("%s", elm.c_str());
+	  // 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());
+        }
+      }
+      // 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);
 
@@ -334,9 +352,6 @@ std::shared_ptr<State> DFSExplorer::next_odpor_state()
     XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
     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()) {
-      return state;
-    }
   }
   return nullptr;
 }
@@ -354,15 +369,19 @@ 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: 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()) {
           switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
             case odpor::WakeupTree::InsertionResult::root: {
-              XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
-                        "the execution prior to event `%u`:",
-                        e_prime, e);
+              XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
+                        "the execution prior to event `%u`(%ld: %.20s):",
+                        e_prime, stack_[e_prime]->get_transition_out()->aid_,
+                        stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
+                        prev_state.get_transition_out()->aid_,
+                        prev_state.get_transition_out()->to_string(true).c_str());
               break;
             }
             case odpor::WakeupTree::InsertionResult::interior_node: {