Add conflict detection to EventSet

Detecting whether or not a collection of events
are in conflict important for computing en(C)
and for K-partial alternatives. We simply
follow the definition of conflicts. More
esoteric methods may exist that are faster,
but for now let's keep it simple: we can always
add those in later incrementally

diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp
index f4ee2e1..a1b7924 100644 (file)
--- a/src/mc/explo/udpor/Configuration.cpp
+++ b/src/mc/explo/udpor/Configuration.cpp
@@ -75,7 +75,7 @@ EventSet Configuration::get_minimally_reproducible_events() const
   // topological ordering that appear in `S`
   EventSet minimally_reproducible_events = EventSet();
 
-  for (const auto& maximal_set : maximal_subsets_iterator_wrapper(*this)) {
+  for (const auto& maximal_set : maximal_subsets_iterator_wrapper<Configuration>(*this)) {
     if (maximal_set.size() > minimally_reproducible_events.size()) {
       minimally_reproducible_events = maximal_set;
     } else {

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index 33442cd..2cdb6fb 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -7,9 +7,10 @@
 #include "src/mc/explo/udpor/Configuration.hpp"
 #include "src/mc/explo/udpor/History.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
 
-#include <iterator>
 #include <stack>
+#include <vector>
 
 namespace simgrid::mc::udpor {
 
@@ -133,13 +134,23 @@ bool EventSet::contains(const History& history) const
 
 bool EventSet::is_maximal() const
 {
+  // A set of events is maximal if no event from
+  // the original set is ruled out when traversing
+  // the history of the events
   const History history(*this);
   return *this == history.get_all_maximal_events();
 }
 
 bool EventSet::is_conflict_free() const
 {
-  return false;
+  const auto begin = maximal_subsets_iterator(*this, std::nullopt, {2});
+  const auto end   = maximal_subsets_iterator();
+  return std::none_of(begin, end, [](const EventSet event_pair) {
+    const auto events        = std::move(event_pair).move_into_vector();
+    const UnfoldingEvent* e1 = events[0];
+    const UnfoldingEvent* e2 = events[1];
+    return e1->conflicts_with(e2);
+  });
 }
 
 std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering() const
@@ -213,4 +224,16 @@ std::vector<const UnfoldingEvent*> EventSet::get_topological_ordering_of_reverse
   return topological_events;
 }
 
+std::vector<const UnfoldingEvent*> EventSet::move_into_vector() const&&
+{
+  std::vector<const UnfoldingEvent*> contents;
+  contents.reserve(size());
+
+  for (auto&& event : *this) {
+    contents.push_back(event);
+  }
+
+  return contents;
+}
+
 } // namespace simgrid::mc::udpor
\ No newline at end of file

diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index 31bd7a9..e49e1db 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -142,6 +142,11 @@ public:
    * closer to the "bottom"
    */
   std::vector<const UnfoldingEvent*> get_topological_ordering_of_reverse_graph() const;
+
+  /**
+   * @brief Moves the event set into a list
+   */
+  std::vector<const UnfoldingEvent*> move_into_vector() const&&;
 };
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 88f4b82..9dffa83 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -40,4 +40,43 @@ EventSet UnfoldingEvent::get_history() const
   return History(this).get_all_events();
 }
 
+bool UnfoldingEvent::related_to(const UnfoldingEvent* other) const
+{
+  return EventSet({this, other}).is_maximal();
+}
+
+bool UnfoldingEvent::in_history_of(const UnfoldingEvent* other) const
+{
+  return History(other).contains(this);
+}
+
+bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const
+{
+  // Events that have a causal relation never are in conflict
+  // in an unfolding structure. Two events in conflict must
+  // not be contained in each other's histories
+  if (related_to(other)) {
+    return false;
+  }
+
+  const EventSet my_history      = get_history();
+  const EventSet other_history   = other->get_history();
+  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;
+}
+
+bool UnfoldingEvent::has_conflicting_transition_with(const UnfoldingEvent* other) const
+{
+  return associated_transition->depends(other->associated_transition.get());
+}
+
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index f19c41e..e6c4662 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.hpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.hpp
@@ -27,11 +27,13 @@ public:
   UnfoldingEvent(UnfoldingEvent&&)                 = default;
 
   EventSet get_history() const;
-  bool in_history_of(const UnfoldingEvent* otherEvent) const;
+  bool in_history_of(const UnfoldingEvent* other) const;
+  bool related_to(const UnfoldingEvent* other) const;
 
-  bool conflicts_with(const UnfoldingEvent* otherEvent) const;
+  bool conflicts_with(const UnfoldingEvent* other) const;
   bool conflicts_with(const Configuration& config) const;
-  bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
+  bool immediately_conflicts_with(const UnfoldingEvent* other) const;
+  bool has_conflicting_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(); }

diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp
index c36d04a..7d0ab46 100644 (file)
--- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp
+++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp
@@ -148,8 +148,8 @@ private:
   friend class boost::iterator_core_access;
 };
 
-using maximal_subsets_iterator_wrapper =
-    simgrid::xbt::iterator_wrapping<maximal_subsets_iterator, const Configuration&>;
+template <typename T>
+using maximal_subsets_iterator_wrapper = simgrid::xbt::iterator_wrapping<maximal_subsets_iterator, const T&>;
 
 } // namespace simgrid::mc::udpor
 #endif