X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d55be44853d961bda7fcbcb20a7952d820d3f3d8..da64c6383731d10c6174f81b4b6a20ff0ea186ae:/src/mc/explo/UdporChecker.cpp diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 6416c49f2b..43c229ff77 100644 --- 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` (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;