Add new entry in Release_Notes.

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

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 6416c49..f5c512f 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -19,7 +19,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification
 
 namespace simgrid::mc::udpor {
 
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args) {}
 
 void UdporChecker::run()
 {
@@ -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;
@@ -294,7 +300,7 @@ void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration
 
   // "U (complicated expression)" portion
   const EventSet conflict_union = std::accumulate(
-      C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet acc, const UnfoldingEvent* e_prime) {
+      C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet& acc, const UnfoldingEvent* e_prime) {
         return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime));
       });