From 619e8feb6e896e993ac5a8a49e15f6fdd5b1e34f Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 15 Mar 2023 09:33:31 +0100 Subject: [PATCH] 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 --- src/mc/explo/udpor/UnfoldingEvent.cpp | 22 +++-- src/mc/explo/udpor/UnfoldingEvent_test.cpp | 96 ++++++++++++++++++++++ src/mc/explo/udpor/Unfolding_test.cpp | 10 +++ src/mc/explo/udpor/udpor_tests_private.hpp | 14 ++++ 4 files changed, 130 insertions(+), 12 deletions(-) diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index 361ed36e2f..1470aac51f 100644 --- 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_ptraid_ != 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 a0a18e92c3..a676c69fdb 100644 --- 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(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e3(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e4(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + + UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared(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(Transition::Type::UNKNOWN, 1, 0)); + UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared(Transition::Type::UNKNOWN, 1, 0)); + UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::ACTOR_JOIN, 0, 0)); + UnfoldingEvent e2_diff_transition(EventSet({&e1}), + std::make_shared(Transition::Type::ACTOR_JOIN, 0, 0)); + UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::UNKNOWN, 0, 1)); + UnfoldingEvent e2_diff_considered(EventSet({&e1}), + std::make_shared(Transition::Type::UNKNOWN, 0, 1)); + UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}), + std::make_shared(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(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared(Transition::Type::UNKNOWN, 0, 0)); + UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}), + std::make_shared(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 72f8602229..19a80dd4f2 100644 --- 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(EventSet(), std::make_shared()); + auto e2 = std::make_unique(EventSet(), std::make_shared()); + + // 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 6e1a23345b..276edfca79 100644 --- 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 { -- 2.20.1