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