+ for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
+ for (const auto& transition : actor_state.get_enabled_transitions()) {
+ // First check for a specialized function that can compute the extension
+ // set "quickly" based on its type. Otherwise, fall back to computing
+ // the set "by hand"
+ const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
+ if (specialized_extension_function != incremental_extension_functions.end()) {
+ exC.form_union((specialized_extension_function->second)(C, transition));
+ } else {
+ exC.form_union(this->compute_exC_by_enumeration(C, transition));
+ }
+ }
+ }
+ return exC;
+}
+
+EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
+{
+ // Here we're computing the following:
+ //
+ // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
+ //
+ // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
+ EventSet incremental_exC;
+
+ for (auto begin =
+ maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
+ begin != maximal_subsets_iterator(); ++begin) {
+ const EventSet& maximal_subset = *begin;
+
+ // TODO: Determine if `a` is enabled here
+ const bool enabled_at_config_k = false;
+
+ if (enabled_at_config_k) {
+ auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
+ if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
+ // This is a new event (i.e. one we haven't yet seen)
+ unfolding.insert(std::move(candidate_handle));
+ incremental_exC.insert(candidate_event);
+ }
+ }
+ }
+
+ return incremental_exC;
+}