Suppressed a bit too much of codes

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 180fe70..0466d66 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -140,16 +140,15 @@ void DFSExplorer::run()
 
     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());
+        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) {
-          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());
+        } 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 --
@@ -351,6 +350,9 @@ 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;
 }

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index 8486a0c..230308f 100644 (file)
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -146,7 +146,7 @@ bool SemaphoreTransition::depends(const Transition* o) const
     if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK)
       return false;
 
-    // UNLCOK indep with a WAIT if the semaphore had enought capacity anyway
+    // UNLOCK indep with a WAIT if the semaphore had enought capacity anyway
     if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT)
       return false;