Merge branch 'master' into 'task-token'

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

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 6416c49f2b6e18ec9a27f038a925d0eb0697f9ee..43c229ff77456272ff7902dcde871dd02c871f0d 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -114,8 +114,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event
     // that we are searching again from `state(C)`. While the
     // stack of states is properly adjusted to represent
     // `state(C)` all together, the RemoteApp is currently sitting
-    // at some *future* state with resepct to `state(C)` since the
-    // recursive calls have moved it there.
+    // at some *future* state with respect to `state(C)` since the
+    // recursive calls had moved it there.
     restore_program_state_with_current_stack();
 
     // Explore(C, D + {e}, J \ C)
@@ -161,10 +161,16 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC,
   // actors in a consistent order since `std::map` is by-default ordered using
   // `std::less<Key>` (see the return type of `State::get_actors_list()`)
   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
-    for (const auto& transition : actor_state.get_enabled_transitions()) {
-      XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
-      EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
-      exC.form_union(extension);
+    const auto& enabled_transitions = actor_state.get_enabled_transitions();
+    if (enabled_transitions.empty()) {
+      XBT_DEBUG("\t Actor `%ld` is disabled: no partial extensions need to be considered", aid);
+    } else {
+      XBT_DEBUG("\t Actor `%ld` is enabled", aid);
+      for (const auto& transition : enabled_transitions) {
+        XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
+        EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
+        exC.form_union(extension);
+      }
     }
   }
   return exC;