Spit a message when ODPOR is not optimal

[simgrid.git] / src / mc / explo / DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 0fb95fd..a7c9dcf 100644 (file)
--- 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,16 @@ 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_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());
+        }
+      }
       // 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(),