Add implementation for immediate conflicts

Two events are said to be in immediate conflict
if they are conflicting but if the removal of
either event from their shared history would
result in a conflict-free set. That is, if
the only conflict among the set of events in
the history of the two events `e` and `e'`
is between `e` and `e'`, then `e` and `e'`
are in immediate conflict

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 50c1e22..0f62179 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -88,6 +88,35 @@ bool UnfoldingEvent::conflicts_with(const Configuration& config) const
                      [&](const UnfoldingEvent* e) { return this->has_dependent_transition_with(e); });
 }
 
+bool UnfoldingEvent::immediately_conflicts_with(const UnfoldingEvent* other) const
+{
+  // They have to be in conflict at a minimum
+  if (not conflicts_with(other)) {
+    return false;
+  }
+
+  auto combined_events = History(EventSet{this, other}).get_all_events();
+
+  // See the definition of immediate conflicts in the original paper on UDPOR
+  {
+    combined_events.remove(this);
+    if (not combined_events.is_valid_configuration()) {
+      return false;
+    }
+    combined_events.insert(this);
+  }
+
+  {
+    combined_events.remove(other);
+    if (not combined_events.is_valid_configuration()) {
+      return false;
+    }
+    combined_events.insert(other);
+  }
+
+  return true;
+}
+
 bool UnfoldingEvent::is_dependent_with(const Transition* t) const
 {
   return associated_transition->depends(t);