Fix logic for mutual conflict between two events

Prior to this commit, detecting whether two
events were in conflict involved looking at all
of the events with respect to all others. However,
you must instead *only* look at how the event `e`
and `e'` relate to the other event's history:
we wouldn't care if some other event is in conflict
with `e'` if `e` is not that event

diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp
index 62109a4..0176118 100644 (file)
--- a/src/mc/explo/udpor/EventSet_test.cpp
+++ b/src/mc/explo/udpor/EventSet_test.cpp
@@ -953,4 +953,102 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Checking conflicts")
     // 6 choose 6 = 1 test
     CHECK_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_conflict_free());
   }
+
+  SECTION("Conditional conflicts")
+  {
+    UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+    UnfoldingEvent e2(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>());
+    UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+    UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
+    UnfoldingEvent e5(EventSet({&e1}), std::make_shared<DependentAction>());
+    UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+
+    // 6 choose 0 = 1 test
+    // There are no events even to be in conflict with
+    CHECK(EventSet().is_conflict_free());
+
+    // 6 choose 1 = 6 tests
+    // Sets of size 1 should still have no conflicts
+    CHECK(EventSet({&e1}).is_conflict_free());
+    CHECK(EventSet({&e2}).is_conflict_free());
+    CHECK(EventSet({&e3}).is_conflict_free());
+    CHECK(EventSet({&e4}).is_conflict_free());
+    CHECK(EventSet({&e5}).is_conflict_free());
+    CHECK(EventSet({&e6}).is_conflict_free());
+
+    // 6 choose 2 = 15 tests
+    CHECK(EventSet({&e1, &e2}).is_conflict_free());
+    CHECK(EventSet({&e1, &e3}).is_conflict_free());
+    CHECK(EventSet({&e1, &e4}).is_conflict_free());
+    CHECK(EventSet({&e1, &e5}).is_conflict_free());
+    CHECK(EventSet({&e1, &e6}).is_conflict_free());
+    CHECK(EventSet({&e2, &e3}).is_conflict_free());
+    CHECK(EventSet({&e2, &e4}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e5}).is_conflict_free());
+
+    // Although e2 and e6 are not directly dependent,
+    // e2 conflicts with e5 which causes e6
+    CHECK_FALSE(EventSet({&e2, &e6}).is_conflict_free());
+    CHECK(EventSet({&e3, &e4}).is_conflict_free());
+
+    // Likewise, since e2 and e5 conflict and e2 causes
+    // e3, so e3 and e5 conflict
+    CHECK_FALSE(EventSet({&e3, &e5}).is_conflict_free());
+    CHECK(EventSet({&e3, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e4, &e5}).is_conflict_free());
+    CHECK(EventSet({&e4, &e6}).is_conflict_free());
+    CHECK(EventSet({&e5, &e6}).is_conflict_free());
+
+    // 6 choose 3 = 20 tests
+    CHECK(EventSet({&e1, &e2, &e3}).is_conflict_free());
+    CHECK(EventSet({&e1, &e2, &e4}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e6}).is_conflict_free());
+    CHECK(EventSet({&e1, &e3, &e4}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e3, &e5}).is_conflict_free());
+    CHECK(EventSet({&e1, &e3, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e4, &e5}).is_conflict_free());
+    CHECK(EventSet({&e1, &e4, &e6}).is_conflict_free());
+    CHECK(EventSet({&e1, &e5, &e6}).is_conflict_free());
+    CHECK(EventSet({&e2, &e3, &e4}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e4, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e3, &e4, &e5}).is_conflict_free());
+    CHECK(EventSet({&e3, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e3, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e4, &e5, &e6}).is_conflict_free());
+
+    // 6 choose 4 = 15 tests
+    CHECK(EventSet({&e1, &e2, &e3, &e4}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e5}).is_conflict_free());
+
+    // e2 is dependent with e6
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e4, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_conflict_free());
+    CHECK(EventSet({&e1, &e3, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_conflict_free());
+
+    // 6 choose 5 = 6 tests
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_conflict_free());
+    CHECK_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_conflict_free());
+
+    // 6 choose 6 = 1 test
+    CHECK_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_conflict_free());
+  }
 }
\ No newline at end of file

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 83e1d7d..fe1a3a3 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -64,14 +64,13 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const
   const EventSet unique_to_me    = my_history.subtracting(other_history);
   const EventSet unique_to_other = other_history.subtracting(my_history);
 
-  for (const auto e_me : unique_to_me) {
-    for (const auto e_other : unique_to_other) {
-      if (e_me->has_conflicting_transition_with(e_other)) {
-        return true;
-      }
-    }
-  }
-  return false;
+  const bool conflicts_with_me = std::any_of(unique_to_me.begin(), unique_to_me.end(), [&](const UnfoldingEvent* e) {
+    return e->has_dependent_transition_with(other);
+  });
+  const bool conflicts_with_other =
+      std::any_of(unique_to_other.begin(), unique_to_other.end(),
+                  [&](const UnfoldingEvent* e) { return e->has_dependent_transition_with(this); });
+  return conflicts_with_me or conflicts_with_other;
 }
 
 bool UnfoldingEvent::conflicts_with(const Configuration& config) const
@@ -83,10 +82,10 @@ bool UnfoldingEvent::conflicts_with(const Configuration& config) const
   // if they are not related)
   const EventSet potential_conflicts = config.get_events().subtracting(get_history());
   return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(),
-                     [&](const UnfoldingEvent* e) { return this->has_conflicting_transition_with(e); });
+                     [&](const UnfoldingEvent* e) { return this->has_dependent_transition_with(e); });
 }
 
-bool UnfoldingEvent::has_conflicting_transition_with(const UnfoldingEvent* other) const
+bool UnfoldingEvent::has_dependent_transition_with(const UnfoldingEvent* other) const
 {
   return associated_transition->depends(other->associated_transition.get());
 }

diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index e6c4662..3ef7d9f 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.hpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.hpp
@@ -33,7 +33,7 @@ public:
   bool conflicts_with(const UnfoldingEvent* other) const;
   bool conflicts_with(const Configuration& config) const;
   bool immediately_conflicts_with(const UnfoldingEvent* other) const;
-  bool has_conflicting_transition_with(const UnfoldingEvent* other) const;
+  bool has_dependent_transition_with(const UnfoldingEvent* other) const;
 
   const EventSet& get_immediate_causes() const { return this->immediate_causes; }
   Transition* get_transition() const { return this->associated_transition.get(); }