From 7ed8d36f850b6cd3de330cf031ebc97539e28262 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 9 Mar 2023 15:34:25 +0100
Subject: [PATCH] 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
---
 src/mc/explo/udpor/UnfoldingEvent.cpp | 29 +++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 50c1e22a51..0f62179b15 100644
--- 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);
-- 
2.20.1