Add semantic equivalence to UnfoldingEvent

Two UnfoldingEvents are considered to be equivalent
if they have the same associated action (same actor,
type, and times_considered) and the same immediate history.
Semantic equivalence is required since any given
event may appear in the extension set of several configurations
that UDPOR decides to explore, and thus we must be able
to determine if a newly-computed event has already been
seen before

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 361ed36..1470aac 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -20,22 +20,20 @@ UnfoldingEvent::UnfoldingEvent(EventSet immediate_causes, std::shared_ptr<Transi
 
 bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
 {
-  // Must be run by the same actor
-  if (associated_transition->aid_ != other.associated_transition->aid_)
-    return false;
-
-  // If run by the same actor, must be the same _step_ of that actor's
-  // execution
-
-  // 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
+  // Two events are equivalent iff:
+  // 1. they have the same action
+  // 2. they have the same history
+  //
+  // NOTE: 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 unfolding 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;
+  return associated_transition->aid_ == other.associated_transition->aid_ &&
+         associated_transition->type_ == other.associated_transition->type_ &&
+         associated_transition->times_considered_ == other.associated_transition->times_considered_ &&
+         this->immediate_causes == other.immediate_causes;
 }
 
 EventSet UnfoldingEvent::get_history() const

diff --git a/src/mc/explo/udpor/UnfoldingEvent_test.cpp b/src/mc/explo/udpor/UnfoldingEvent_test.cpp
index a0a18e9..a676c69 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent_test.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent_test.cpp
@@ -7,8 +7,104 @@
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/explo/udpor/udpor_tests_private.hpp"
 
+using namespace simgrid::mc;
 using namespace simgrid::mc::udpor;
 
+TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Semantic Equivalence Tests")
+{
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+  UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+  UnfoldingEvent e4(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+  UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+  UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+  UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+  SECTION("Equivalence is an equivalence relation")
+  {
+    SECTION("Equivalence is reflexive")
+    {
+      REQUIRE(e1 == e1);
+      REQUIRE(e2 == e2);
+      REQUIRE(e3 == e3);
+      REQUIRE(e4 == e4);
+    }
+
+    SECTION("Equivalence is symmetric")
+    {
+      REQUIRE(e2 == e3);
+      REQUIRE(e3 == e2);
+      REQUIRE(e3 == e4);
+      REQUIRE(e4 == e3);
+      REQUIRE(e2 == e4);
+      REQUIRE(e4 == e2);
+    }
+
+    SECTION("Equivalence is transitive")
+    {
+      REQUIRE(e2 == e3);
+      REQUIRE(e3 == e4);
+      REQUIRE(e2 == e4);
+      REQUIRE(e5 == e6);
+      REQUIRE(e6 == e7);
+      REQUIRE(e5 == e7);
+    }
+  }
+
+  SECTION("Equivalence fails with different actors")
+  {
+    UnfoldingEvent e1_diff_actor(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+    UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+    UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}),
+                                 std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1, 0));
+    REQUIRE(e1 != e1_diff_actor);
+    REQUIRE(e1 != e2_diff_actor);
+    REQUIRE(e1 != e5_diff_actor);
+  }
+
+  SECTION("Equivalence fails with different transition types")
+  {
+    // NOTE: We're comparing the transition `type_` field directly. To avoid
+    // modifying the `Type` enum that exists in `Transition` just for the tests,
+    // we instead provide different values of `Transition::Type` to simulate
+    // the different types
+    UnfoldingEvent e1_diff_transition(EventSet(),
+                                      std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+    UnfoldingEvent e2_diff_transition(EventSet({&e1}),
+                                      std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+    UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}),
+                                      std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+    REQUIRE(e1 != e1_diff_transition);
+    REQUIRE(e1 != e2_diff_transition);
+    REQUIRE(e1 != e5_diff_transition);
+  }
+
+  SECTION("Equivalence fails with different `times_considered`")
+  {
+    // With a different number for `times_considered`, we know
+    UnfoldingEvent e1_diff_considered(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+    UnfoldingEvent e2_diff_considered(EventSet({&e1}),
+                                      std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+    UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}),
+                                      std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+    REQUIRE(e1 != e1_diff_considered);
+    REQUIRE(e1 != e2_diff_considered);
+    REQUIRE(e1 != e5_diff_considered);
+  }
+
+  SECTION("Equivalence fails with different immediate histories of events")
+  {
+    UnfoldingEvent e1_diff_hist(EventSet({&e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+    UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+    UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}),
+                                std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+    REQUIRE(e1 != e1_diff_hist);
+    REQUIRE(e1 != e2_diff_hist);
+    REQUIRE(e1 != e5_diff_hist);
+  }
+}
+
 TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Dependency/Conflict Tests")
 {
   SECTION("Properties of the relations")

diff --git a/src/mc/explo/udpor/Unfolding_test.cpp b/src/mc/explo/udpor/Unfolding_test.cpp
index 72f8602..19a80dd 100644 (file)
--- a/src/mc/explo/udpor/Unfolding_test.cpp
+++ b/src/mc/explo/udpor/Unfolding_test.cpp
@@ -39,4 +39,14 @@ TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an
   unfolding.remove(e2_handle);
   REQUIRE(unfolding.size() == 0);
   REQUIRE(unfolding.empty());
+}
+
+TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
+{
+  Unfolding unfolding;
+  auto e1 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<IndependentAction>());
+  auto e2 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<IndependentAction>());
+
+  // e1 and e2 are semantically equivalent
+  REQUIRE(*e1 == *e2);
 }
\ No newline at end of file

diff --git a/src/mc/explo/udpor/udpor_tests_private.hpp b/src/mc/explo/udpor/udpor_tests_private.hpp
index 6e1a233..276edfc 100644 (file)
--- a/src/mc/explo/udpor/udpor_tests_private.hpp
+++ b/src/mc/explo/udpor/udpor_tests_private.hpp
@@ -12,14 +12,22 @@
 #ifndef SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
 #define SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
 
+#include "src/mc/transition/Transition.hpp"
+
 namespace simgrid::mc::udpor {
 
 struct IndependentAction : public Transition {
+  IndependentAction() = default;
+  IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
   // Independent with everyone else
   bool depends(const Transition* other) const override { return false; }
 };
 
 struct DependentAction : public Transition {
+  DependentAction() = default;
+  DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+
   // Dependent with everyone else (except IndependentAction)
   bool depends(const Transition* other) const override
   {
@@ -28,6 +36,12 @@ struct DependentAction : public Transition {
 };
 
 struct ConditionallyDependentAction : public Transition {
+  ConditionallyDependentAction() = default;
+  ConditionallyDependentAction(Type type, aid_t issuer, int times_considered)
+      : Transition(type, issuer, times_considered)
+  {
+  }
+
   // Dependent only with DependentAction (i.e. not itself)
   bool depends(const Transition* other) const override
   {