X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1d2749010b8bc3bd6338abed1c4cbc2fdd9a8895..e80fc92c523fadeda71f4f7c2f0ca6a5a7dea7a7:/src/mc/explo/UdporChecker.cpp

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 3221c2ac47..f5c512f480 100644
--- 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()
 {
@@ -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));
       });