Only compute extensions for enabled events

diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp
index 2e8e136..ed40454 100644 (file)
--- a/src/mc/api/ActorState.hpp
+++ b/src/mc/api/ActorState.hpp
@@ -164,7 +164,8 @@ public:
 
   const std::vector<std::shared_ptr<Transition>>& get_enabled_transitions() const
   {
-    return this->pending_transitions_;
+    static const auto no_enabled_transitions = std::vector<std::shared_ptr<Transition>>();
+    return this->is_enabled() ? this->pending_transitions_ : no_enabled_transitions;
   };
 };
 

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index 3221c2a..43c229f 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -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;