From: Maxwell Pirtle Date: Thu, 9 Mar 2023 13:08:27 +0000 (+0100) Subject: Add test to verify topological ordering of EventSet X-Git-Tag: v3.34~350^2~5 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/764829f87878f239dc6173d0201b5249531da2db Add test to verify topological ordering of EventSet The topological ordering was moved into EventSet in a prior commit since it is useful to order events in an EventSet that reside outside of a Configuration. This commit adds a stress test that verifies that the topological orderings of all possible subsets of a collection of events obey the topological ordering invariant after being ordered (in both directions) --- diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index d4ed132623..c6e755be79 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -148,7 +148,9 @@ public: */ std::vector move_into_vector() const&&; - using const_iterator = std::unordered_set::const_iterator; + using iterator = decltype(events_)::iterator; + using const_iterator = decltype(events_)::const_iterator; + using value_type = decltype(events_)::value_type; }; } // namespace simgrid::mc::udpor diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp index 0176118e01..776d3b3ce4 100644 --- a/src/mc/explo/udpor/EventSet_test.cpp +++ b/src/mc/explo/udpor/EventSet_test.cpp @@ -5,10 +5,12 @@ #include "src/3rd-party/catch.hpp" #include "src/mc/explo/udpor/EventSet.hpp" +#include "src/mc/explo/udpor/History.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" #include "src/mc/explo/udpor/udpor_tests_private.hpp" -#include "src/mc/transition/Transition.hpp" +#include "src/xbt/utils/iter/LazyPowerset.hpp" +using namespace simgrid::xbt; using namespace simgrid::mc::udpor; TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets") @@ -1051,4 +1053,77 @@ 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()); } +} + +TEST_CASE("simgrid::mc::udpor::EventSet: Topological Ordering Property Observed for Every Possible Subset") +{ + // The following tests concern the given event structure: + // e1 + // / / + // e2 e6 + // / / / + // e3 / / + // / / / + // e4 e5 e7 + UnfoldingEvent e1(EventSet(), std::make_shared()); + UnfoldingEvent e2(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e3(EventSet({&e2}), std::make_shared()); + UnfoldingEvent e4(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e5(EventSet({&e3}), std::make_shared()); + UnfoldingEvent e6(EventSet({&e1}), std::make_shared()); + UnfoldingEvent e7(EventSet({&e2, &e6}), std::make_shared()); + + const EventSet all_events{&e1, &e2, &e3, &e4, &e5, &e6, &e7}; + + for (const auto& subset_of_iterators : make_powerset_iter(all_events)) { + // Verify that the topological ordering property holds for every subset + + const EventSet subset = [&subset_of_iterators]() { + EventSet subset_local; + for (const auto iter : subset_of_iterators) { + subset_local.insert(*iter); + } + return subset_local; + }(); + + { + // To test this, we verify that at each point none of the events + // that follow after any particular event `e` are contained in + // `e`'s history + EventSet invalid_events = subset; + const auto ordered_events = subset.get_topological_ordering(); + + std::for_each(ordered_events.begin(), ordered_events.end(), [&](const UnfoldingEvent* e) { + History history(e); + for (auto* e_hist : history) { + if (e_hist == e) + continue; + REQUIRE_FALSE(invalid_events.contains(e_hist)); + } + invalid_events.remove(e); + }); + } + { + // To test this, we verify that at each point none of the events + // that we've processed in the ordering are ever seen again + // in anybody else's history + EventSet events_seen; + const auto ordered_events = subset.get_topological_ordering_of_reverse_graph(); + + std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) { + History history(e); + + for (auto* e_hist : history) { + // Unlike the test above, we DO want to ensure + // that `e` itself ALSO isn't yet seen + + // If this event has been "seen" before, + // this implies that event `e` appears later + // in the list than one of its ancestors + REQUIRE_FALSE(events_seen.contains(e_hist)); + } + events_seen.insert(e); + }); + } + } } \ No newline at end of file diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index b72e13c987..b6d9b37eca 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -40,6 +40,7 @@ public: Transition* get_transition() const { return this->associated_transition.get(); } bool operator==(const UnfoldingEvent&) const; + bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); } /** * @brief The transition that UDPOR "attaches" to this diff --git a/src/mc/explo/udpor/Unfolding_test.cpp b/src/mc/explo/udpor/Unfolding_test.cpp index 4e6f627309..72f8602229 100644 --- a/src/mc/explo/udpor/Unfolding_test.cpp +++ b/src/mc/explo/udpor/Unfolding_test.cpp @@ -5,6 +5,7 @@ #include "src/3rd-party/catch.hpp" #include "src/mc/explo/udpor/Unfolding.hpp" +#include "src/mc/explo/udpor/udpor_tests_private.hpp" using namespace simgrid::mc::udpor; @@ -18,10 +19,10 @@ TEST_CASE("simgrid::mc::udpor::Unfolding: Creating an unfolding") TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding") { Unfolding unfolding; - auto e1 = std::make_unique(); - auto e2 = std::make_unique(); - auto e1_handle = e1.get(); - auto e2_handle = e2.get(); + auto e1 = std::make_unique(); + auto e2 = std::make_unique(); + const auto e1_handle = e1.get(); + const auto e2_handle = e2.get(); unfolding.insert(std::move(e1)); REQUIRE(unfolding.size() == 1);