+
+ // Remove(e, C, D)
+ clean_up_explore(e, C, D);
+}
+
+EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
+{
+ // See eqs. 5.7 of section 5.2 of [3]
+ // C = C' + {e_cur}, i.e. C' = C - {e_cur}
+ //
+ // Then
+ //
+ // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
+ // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
+ const UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
+ exC.remove(e_cur);
+
+ for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
+ for (const auto& transition : actor_state.get_enabled_transitions()) {
+ EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
+ exC.form_union(extension);
+ }
+ }
+ return exC;