- std::stack<UnfoldingEvent*> event_stack;
- std::vector<UnfoldingEvent*> topological_ordering;
- EventSet unknown_events = events_, temporarily_marked_events, permanently_marked_events;
-
- while (not unknown_events.empty()) {
- EventSet discovered_events;
- event_stack.push(*unknown_events.begin());
-
- while (not event_stack.empty()) {
- UnfoldingEvent* evt = event_stack.top();
- discovered_events.insert(evt);
-
- if (not temporarily_marked_events.contains(evt)) {
- // If this event hasn't yet been marked, do
- // so now so that if we see it again in a child we can
- // detect a cycle and if we see it again here
- // we can detect that the node is re-processed
- temporarily_marked_events.insert(evt);
-
- EventSet immediate_causes = evt->get_immediate_causes();
- if (!immediate_causes.empty() && immediate_causes.is_subset_of(temporarily_marked_events)) {
- throw std::invalid_argument("Attempted to perform a topological sort on a configuration "
- "whose contents contain a cycle. The configuration (and the graph "
- "connecting all of the events) is an invalid event structure");
- }
- immediate_causes.subtract(discovered_events);
- immediate_causes.subtract(permanently_marked_events);
- const EventSet undiscovered_causes = std::move(immediate_causes);
-
- for (const auto cause : undiscovered_causes) {
- event_stack.push(cause);
- }
- } else {
- // Mark this event as:
- // 1. discovered across all DFSs performed
- // 2. permanently marked
- // 3. part of the topological search
- unknown_events.remove(evt);
- temporarily_marked_events.remove(evt);
- permanently_marked_events.insert(evt);
-
- // In moving this event to the end of the list,
- // we are saying this events "happens before" other
- // events that are added later.
- topological_ordering.push_back(evt);
-
- // Only now do we remove the event, i.e. once
- // we've processed the same event again
- event_stack.pop();
- }
- }
+bool Configuration::is_compatible_with(const History& history) const
+{
+ // Note: We don't need to check if the `C` will be causally-closed
+ // after adding `history` to it since a) `C` itself is already
+ // causally-closed and b) the history is already causally closed
+ const auto event_diff = history.get_event_diff_with(*this);
+
+ // The events that are contained outside of the configuration
+ // must themselves be free of conflicts.
+ if (not event_diff.is_conflict_free()) {
+ return false;