+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);
+ }
+ }
+ }