Introduce extrinsic equivalence between events

Extrinsic equivalence between two UnfoldingEvents
simply means that we consider to events to be
"the same". This equivalence is used when UDPOR
creates a new event to determine if in fact that
event has already been created. This requires determining
the equivalence between the transitions associated with
those events as well as the dependencies of each of
the events.

diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index b7e2ef5..f59593e 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -27,8 +27,10 @@ public:
   explicit EventSet(std::unordered_set<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
   explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
 
-  inline auto begin() const { return this->events_.begin(); }
-  inline auto end() const { return this->events_.end(); }
+  auto begin() const { return this->events_.begin(); }
+  auto end() const { return this->events_.end(); }
+  auto cbegin() const { return this->events_.cbegin(); }
+  auto cend() const { return this->events_.cend(); }
 
   void remove(UnfoldingEvent*);
   void subtract(const EventSet&);

diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp
index df5cb32..554b1c3 100644 (file)
--- a/src/mc/explo/udpor/History.hpp
+++ b/src/mc/explo/udpor/History.hpp
@@ -79,8 +79,6 @@ public:
    * dependency graph for all events in this history
    */
   EventSet get_all_events() const;
-
-  EventSet get_event_diff_with(const EventSet& event_set) const;
   EventSet get_event_diff_with(const Configuration& config) const;
 };
 

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index a2ab912..c3f8698 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -13,10 +13,21 @@ UnfoldingEvent::UnfoldingEvent(std::shared_ptr<Transition> transition, EventSet
 {
 }
 
-bool UnfoldingEvent::operator==(const UnfoldingEvent&) const
+bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
 {
-  // TODO: Implement semantic equality
-  return false;
+  const bool same_actor = associated_transition->aid_ == other.associated_transition->aid_;
+  if (!same_actor)
+    return false;
+
+  // TODO: Add in information to determine which step in the sequence this actor was executed
+
+  // All unfolding event objects are created in reference to
+  // an Unfolding object which owns them. Hence, the references
+  // they contain to other events in the unvolding can
+  // be used as intrinsic identities (i.e. we don't need to
+  // recursively check if each of our causes has a `==` in
+  // the other event's causes)
+  return this->immediate_causes == other.immediate_causes;
 }
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index d7a03e1..1a9bae5 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.hpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.hpp
@@ -31,6 +31,7 @@ public:
   bool conflicts_with(const Configuration& config) const;
   bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
 
+  const EventSet& get_immediate_causes() const { return this->immediate_causes; }
   Transition* get_transition() const { return this->associated_transition.get(); }
 
   bool operator==(const UnfoldingEvent&) const;