+
+ // Remove(e, C, D)
+ clean_up_explore(e, C, D);
+}
+
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const
+{
+ // 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, > : H }
+ UnfoldingEvent* e_cur = C.get_latest_event();
+ EventSet exC = prev_exC;
+ exC.remove(e_cur);
+
+ // ... fancy computations
+
+ EventSet enC;
+ return std::tuple<EventSet, EventSet>(exC, enC);
+}
+
+void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
+{
+ const aid_t next_actor = e.get_transition()->aid_;
+
+ // TODO: Add the trace if possible for reporting a bug
+ xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
+ "In reaching this execution path, UDPOR ensures that at least one\n"
+ "one transition of the state of an visited event is enabled, yet no\n"
+ "state was actually enabled. Please report this as a bug.\n"
+ "*********************************\n\n");
+ state.execute_next(next_actor);
+}
+
+void UdporChecker::restore_program_state_to(const State& stateC)
+{
+ // TODO: Perform state regeneration in the same manner as is done
+ // in the DFSChecker.cpp