From: Maxwell Pirtle Date: Thu, 2 Mar 2023 09:00:42 +0000 (+0100) Subject: Pass references to `const Unfolding*` in most places X-Git-Tag: v3.34~372^2~5 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5f4fec5323389b31285cd4e19a6abda90e63a555?hp=61a8bb9423361cde6dfc57a00815e5fc99320ca4 Pass references to `const Unfolding*` in most places Passing references to `const Unfolding*` is better style as no methods actually modify events directly: instead, they perform computations over sets of events, compute histories, etc, but leave the event instances themselves otherwise unaffected --- diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 8a298fbc5a..02452aadb3 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -73,7 +73,7 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std:: // TODO: Add verbose logging about which event is being explored - UnfoldingEvent* e = select_next_unfolding_event(A, enC); + const UnfoldingEvent* e = select_next_unfolding_event(A, enC); xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n" "UDPOR guarantees that an event will be chosen at each point in\n" "the search, yet no events were actually chosen\n" @@ -128,8 +128,8 @@ std::tuple UdporChecker::compute_extension(const Configurati // // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + // U{ : K is maximal, `a` depends on all of K, `a` enabled at K } - UnfoldingEvent* e_cur = C.get_latest_event(); - EventSet exC = prev_exC; + const UnfoldingEvent* e_cur = C.get_latest_event(); + EventSet exC = prev_exC; exC.remove(e_cur); for (const auto& [aid, actor_state] : stateC.get_actors_list()) { @@ -195,7 +195,7 @@ std::unique_ptr UdporChecker::record_current_state() return next_state; } -UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) +const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC) { if (!enC.empty()) { return *(enC.begin()); diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 30407c4217..5e0b575a5f 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -115,7 +115,7 @@ private: * by the UDPOR algorithm to select new events to search. See the original * paper [1] for more details */ - UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); + const UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); /** * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp index a05d3a7a0a..70f4659f0b 100644 --- a/src/mc/explo/udpor/Configuration.cpp +++ b/src/mc/explo/udpor/Configuration.cpp @@ -14,7 +14,8 @@ namespace simgrid::mc::udpor { -Configuration::Configuration(std::initializer_list events) : Configuration(EventSet(std::move(events))) +Configuration::Configuration(std::initializer_list events) + : Configuration(EventSet(std::move(events))) { } @@ -25,7 +26,7 @@ Configuration::Configuration(const EventSet& events) : events_(events) } } -void Configuration::add_event(UnfoldingEvent* e) +void Configuration::add_event(const UnfoldingEvent* e) { if (e == nullptr) { throw std::invalid_argument("Expected a nonnull `UnfoldingEvent*` but received NULL instead"); @@ -46,14 +47,14 @@ void Configuration::add_event(UnfoldingEvent* e) } } -std::vector Configuration::get_topologically_sorted_events() const +std::vector Configuration::get_topologically_sorted_events() const { if (events_.empty()) { - return std::vector(); + return std::vector(); } - std::stack event_stack; - std::vector topological_ordering; + std::stack event_stack; + std::vector topological_ordering; EventSet unknown_events = events_; EventSet temporarily_marked_events; EventSet permanently_marked_events; @@ -63,7 +64,7 @@ std::vector Configuration::get_topologically_sorted_events() co event_stack.push(*unknown_events.begin()); while (not event_stack.empty()) { - UnfoldingEvent* evt = event_stack.top(); + const UnfoldingEvent* evt = event_stack.top(); discovered_events.insert(evt); if (not temporarily_marked_events.contains(evt)) { @@ -109,7 +110,7 @@ std::vector Configuration::get_topologically_sorted_events() co return topological_ordering; } -std::vector Configuration::get_topologically_sorted_events_of_reverse_graph() const +std::vector Configuration::get_topologically_sorted_events_of_reverse_graph() const { // The method exploits the property that // a topological sorting S^R of the reverse graph G^R diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp index 8b2c219df6..a820a41f91 100644 --- a/src/mc/explo/udpor/Configuration.hpp +++ b/src/mc/explo/udpor/Configuration.hpp @@ -9,8 +9,10 @@ #include "src/mc/explo/udpor/EventSet.hpp" #include "src/mc/explo/udpor/udpor_forward.hpp" +#include #include #include +#include #include namespace simgrid::mc::udpor { @@ -23,14 +25,14 @@ public: Configuration(Configuration&&) = default; explicit Configuration(const EventSet& events); - explicit Configuration(std::initializer_list events); + explicit Configuration(std::initializer_list events); auto begin() const { return this->events_.begin(); } auto end() const { return this->events_.end(); } - bool contains(UnfoldingEvent* e) const { return this->events_.contains(e); } + bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); } const EventSet& get_events() const { return this->events_; } - UnfoldingEvent* get_latest_event() const { return this->newest_event; } + const UnfoldingEvent* get_latest_event() const { return this->newest_event; } /** * @brief Insert a new event into the configuration @@ -59,7 +61,7 @@ public: * we shouldn't focus so much on this (let alone the additional benefit of the * assertions) */ - void add_event(UnfoldingEvent* e); + void add_event(const UnfoldingEvent* e); /** * @brief Orders the events of the configuration such that @@ -76,7 +78,7 @@ public: * structure appear farther along in the list than those that appear * closer to the "top" */ - std::vector get_topologically_sorted_events() const; + std::vector get_topologically_sorted_events() const; /** * @brief Orders the events of the configuration such that @@ -100,13 +102,13 @@ public: * structure appear farther along in the list than those that appear * closer to the "bottom" */ - std::vector get_topologically_sorted_events_of_reverse_graph() const; + std::vector get_topologically_sorted_events_of_reverse_graph() const; private: /** * @brief The most recent event added to the configuration */ - UnfoldingEvent* newest_event = nullptr; + const UnfoldingEvent* newest_event = nullptr; /** * @brief The events which make up this configuration diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp index f9d025ea83..fdfc9147b5 100644 --- a/src/mc/explo/udpor/Configuration_test.cpp +++ b/src/mc/explo/udpor/Configuration_test.cpp @@ -141,8 +141,9 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order") SECTION("Topological ordering for entire set") { Configuration C{&e1, &e2, &e3, &e4}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e4, &e3, &e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == + std::vector{&e4, &e3, &e2, &e1}); } SECTION("Topological ordering for subsets") @@ -150,29 +151,30 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order") SECTION("No elements") { Configuration C; - REQUIRE(C.get_topologically_sorted_events() == std::vector{}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{}); } SECTION("e1 only") { Configuration C{&e1}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e1}); } SECTION("e1 and e2 only") { Configuration C{&e1, &e2}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e2, &e1}); } SECTION("e1, e2, and e3 only") { Configuration C{&e1, &e2, &e3}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e3, &e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == + std::vector{&e3, &e2, &e1}); } } } @@ -201,51 +203,54 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli SECTION("No elements") { Configuration C; - REQUIRE(C.get_topologically_sorted_events() == std::vector{}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{}); } SECTION("e1 only") { Configuration C{&e1}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e1}); } SECTION("e1 and e2 only") { Configuration C{&e1, &e2}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e2, &e1}); } SECTION("e1, e2, and e3 only") { Configuration C{&e1, &e2, &e3}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e3, &e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == + std::vector{&e3, &e2, &e1}); } SECTION("e1, e2, e3, and e6 only") { Configuration C{&e1, &e2, &e3, &e6}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e6, &e3, &e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == + std::vector{&e6, &e3, &e2, &e1}); } SECTION("e1, e2, e3, and e4 only") { Configuration C{&e1, &e2, &e3, &e4}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4}); - REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector{&e4, &e3, &e2, &e1}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4}); + REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == + std::vector{&e4, &e3, &e2, &e1}); } SECTION("e1, e2, e3, e4, and e5 only") { Configuration C{&e1, &e2, &e3, &e4, &e5}; - REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e5}); + REQUIRE(C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e5}); REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e5, &e4, &e3, &e2, &e1}); + std::vector{&e5, &e4, &e3, &e2, &e1}); } SECTION("e1, e2, e3, e4 and e6 only") @@ -253,12 +258,12 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli // In this case, e4 and e6 are interchangeable. Hence, we have to check // if the sorting gives us *any* of the combinations Configuration C{&e1, &e2, &e3, &e4, &e6}; - REQUIRE((C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e6} || - C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6, &e4})); + REQUIRE((C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e6} || + C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6, &e4})); REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e6, &e4, &e3, &e2, &e1} || + std::vector{&e6, &e4, &e3, &e2, &e1} || C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e4, &e6, &e3, &e2, &e1})); + std::vector{&e4, &e6, &e3, &e2, &e1})); } SECTION("Topological ordering for entire set") @@ -266,15 +271,16 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli // In this case, e4/e5 are both interchangeable with e6. Hence, again we have to check // if the sorting gives us *any* of the combinations Configuration C{&e1, &e2, &e3, &e4, &e5, &e6}; - REQUIRE((C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e5, &e6} || - C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e6, &e5} || - C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6, &e4, &e5})); + REQUIRE( + (C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e5, &e6} || + C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e4, &e6, &e5} || + C.get_topologically_sorted_events() == std::vector{&e1, &e2, &e3, &e6, &e4, &e5})); REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e6, &e5, &e4, &e3, &e2, &e1} || + std::vector{&e6, &e5, &e4, &e3, &e2, &e1} || C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e5, &e6, &e4, &e3, &e2, &e1} || + std::vector{&e5, &e6, &e4, &e3, &e2, &e1} || C.get_topologically_sorted_events_of_reverse_graph() == - std::vector{&e5, &e4, &e6, &e3, &e2, &e1})); + std::vector{&e5, &e4, &e6, &e3, &e2, &e1})); } } } @@ -316,7 +322,7 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli EventSet events_seen; const auto ordered_events = C.get_topologically_sorted_events(); - std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) { + std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) { History history(e); for (auto* e_hist : history) { // In this demo, we want to make sure that @@ -343,7 +349,7 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli EventSet events_seen; const auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph(); - std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) { + std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) { History history(e); for (auto* e_hist : history) { diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp index c0f0195467..5417103f13 100644 --- a/src/mc/explo/udpor/EventSet.cpp +++ b/src/mc/explo/udpor/EventSet.cpp @@ -13,7 +13,7 @@ namespace simgrid::mc::udpor { EventSet::EventSet(Configuration&& config) : EventSet(config.get_events()) {} -void EventSet::remove(UnfoldingEvent* e) +void EventSet::remove(const UnfoldingEvent* e) { this->events_.erase(e); } @@ -30,9 +30,9 @@ void EventSet::subtract(const Configuration& config) EventSet EventSet::subtracting(const EventSet& other) const { - std::unordered_set result = this->events_; + std::unordered_set result = this->events_; - for (UnfoldingEvent* e : other.events_) + for (const UnfoldingEvent* e : other.events_) result.erase(e); return EventSet(std::move(result)); @@ -43,14 +43,14 @@ EventSet EventSet::subtracting(const Configuration& config) const return subtracting(config.get_events()); } -EventSet EventSet::subtracting(UnfoldingEvent* e) const +EventSet EventSet::subtracting(const UnfoldingEvent* e) const { auto result = this->events_; result.erase(e); return EventSet(std::move(result)); } -void EventSet::insert(UnfoldingEvent* e) +void EventSet::insert(const UnfoldingEvent* e) { this->events_.insert(e); } @@ -65,7 +65,7 @@ void EventSet::form_union(const Configuration& config) form_union(config.get_events()); } -EventSet EventSet::make_union(UnfoldingEvent* e) const +EventSet EventSet::make_union(const UnfoldingEvent* e) const { auto result = this->events_; result.insert(e); @@ -74,9 +74,9 @@ EventSet EventSet::make_union(UnfoldingEvent* e) const EventSet EventSet::make_union(const EventSet& other) const { - std::unordered_set result = this->events_; + std::unordered_set result = this->events_; - for (UnfoldingEvent* e : other.events_) + for (const UnfoldingEvent* e : other.events_) result.insert(e); return EventSet(std::move(result)); @@ -97,7 +97,7 @@ bool EventSet::empty() const return this->events_.empty(); } -bool EventSet::contains(UnfoldingEvent* e) const +bool EventSet::contains(const UnfoldingEvent* e) const { return this->events_.find(e) != this->events_.end(); } @@ -126,7 +126,7 @@ bool EventSet::is_valid_configuration() const bool EventSet::contains(const History& history) const { - return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); }); + return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); }); } bool EventSet::is_maximal_event_set() const diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp index 26a910a7d6..4c64746982 100644 --- a/src/mc/explo/udpor/EventSet.hpp +++ b/src/mc/explo/udpor/EventSet.hpp @@ -16,7 +16,7 @@ namespace simgrid::mc::udpor { class EventSet { private: - std::unordered_set events_; + std::unordered_set events_; public: EventSet() = default; @@ -25,31 +25,31 @@ public: EventSet& operator=(EventSet&&) = default; EventSet(EventSet&&) = default; explicit EventSet(Configuration&& config); - explicit EventSet(std::unordered_set&& raw_events) : events_(raw_events) {} - explicit EventSet(std::initializer_list event_list) : events_(std::move(event_list)) {} + explicit EventSet(std::unordered_set&& raw_events) : events_(raw_events) {} + explicit EventSet(std::initializer_list event_list) : events_(std::move(event_list)) {} 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 remove(const UnfoldingEvent*); void subtract(const EventSet&); void subtract(const Configuration&); - EventSet subtracting(UnfoldingEvent*) const; + EventSet subtracting(const UnfoldingEvent*) const; EventSet subtracting(const EventSet&) const; EventSet subtracting(const Configuration&) const; - void insert(UnfoldingEvent*); + void insert(const UnfoldingEvent*); void form_union(const EventSet&); void form_union(const Configuration&); - EventSet make_union(UnfoldingEvent*) const; + EventSet make_union(const UnfoldingEvent*) const; EventSet make_union(const EventSet&) const; EventSet make_union(const Configuration&) const; size_t size() const; bool empty() const; - bool contains(UnfoldingEvent*) const; + bool contains(const UnfoldingEvent*) const; bool contains(const History&) const; bool is_subset_of(const EventSet&) const; diff --git a/src/mc/explo/udpor/History.cpp b/src/mc/explo/udpor/History.cpp index 313b46458f..d9d43d3133 100644 --- a/src/mc/explo/udpor/History.cpp +++ b/src/mc/explo/udpor/History.cpp @@ -24,7 +24,7 @@ void History::Iterator::increment() { if (not frontier.empty()) { // "Pop" the event at the "front" - UnfoldingEvent* e = *frontier.begin(); + const UnfoldingEvent* e = *frontier.begin(); frontier.remove(e); // If there is a configuration and if the @@ -49,7 +49,7 @@ void History::Iterator::increment() } } -UnfoldingEvent* const& History::Iterator::dereference() const +const UnfoldingEvent* const& History::Iterator::dereference() const { return *frontier.begin(); } diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp index 2deb65563c..da35244ef9 100644 --- a/src/mc/explo/udpor/History.hpp +++ b/src/mc/explo/udpor/History.hpp @@ -54,8 +54,8 @@ public: History& operator=(History const&) = default; History(History&&) = default; - explicit History(UnfoldingEvent* e) : events_({e}) {} explicit History(EventSet event_set = EventSet()) : events_(std::move(event_set)) {} + explicit History(const UnfoldingEvent* e) : events_({e}) {} auto begin() const { return Iterator(events_); } auto end() const { return Iterator(EventSet()); } @@ -100,7 +100,7 @@ private: /** * @brief An iterator which traverses the history of a set of events */ - struct Iterator : boost::iterator_facade { + struct Iterator : boost::iterator_facade { public: using optional_configuration = std::optional>; Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt); @@ -122,7 +122,7 @@ private: void increment(); bool equal(const Iterator& other) const; - UnfoldingEvent* const& dereference() const; + const UnfoldingEvent* const& dereference() const; // Allows boost::iterator_facade<...> to function properly friend class boost::iterator_core_access; diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp index 5ca2229d04..88f4b82dc7 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.cpp +++ b/src/mc/explo/udpor/UnfoldingEvent.cpp @@ -8,7 +8,7 @@ namespace simgrid::mc::udpor { -UnfoldingEvent::UnfoldingEvent(std::initializer_list init_list) +UnfoldingEvent::UnfoldingEvent(std::initializer_list init_list) : UnfoldingEvent(EventSet(std::move(init_list))) { } @@ -35,7 +35,7 @@ bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const return this->immediate_causes == other.immediate_causes; } -EventSet UnfoldingEvent::get_history() +EventSet UnfoldingEvent::get_history() const { return History(this).get_all_events(); } diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp index edd7eece88..f19c41eb68 100644 --- a/src/mc/explo/udpor/UnfoldingEvent.hpp +++ b/src/mc/explo/udpor/UnfoldingEvent.hpp @@ -18,7 +18,7 @@ namespace simgrid::mc::udpor { class UnfoldingEvent { public: - explicit UnfoldingEvent(std::initializer_list init_list); + explicit UnfoldingEvent(std::initializer_list init_list); UnfoldingEvent(EventSet immediate_causes = EventSet(), std::shared_ptr transition = std::make_unique()); @@ -26,7 +26,7 @@ public: UnfoldingEvent& operator=(UnfoldingEvent const&) = default; UnfoldingEvent(UnfoldingEvent&&) = default; - EventSet get_history(); + EventSet get_history() const; bool in_history_of(const UnfoldingEvent* otherEvent) const; bool conflicts_with(const UnfoldingEvent* otherEvent) const; diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.cpp b/src/mc/explo/udpor/maximal_subsets_iterator.cpp index a96287d6d6..a811401fa5 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.cpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.cpp @@ -58,18 +58,25 @@ void maximal_subsets_iterator::increment() // Otherwise we found some other event `e'` which is not in conflict with anything // that currently exists in `current_maximal_set`. Add it in and perform // some more bookkeeping - UnfoldingEvent* next_event = *next_event_ref; - add_element_to_current_maximal_set(next_event); + add_element_to_current_maximal_set(*next_event_ref); backtrack_points.push(next_event_ref); } -void maximal_subsets_iterator::add_element_to_current_maximal_set(UnfoldingEvent* e) +bool maximal_subsets_iterator::bookkeeper::is_candidate_event(const UnfoldingEvent* e) const +{ + if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) { + return e_count->second == 0; + } + return true; +} + +void maximal_subsets_iterator::add_element_to_current_maximal_set(const UnfoldingEvent* e) { current_maximal_set.insert(e); bookkeeper.mark_included_in_maximal_set(e); } -void maximal_subsets_iterator::remove_element_from_current_maximal_set(UnfoldingEvent* e) +void maximal_subsets_iterator::remove_element_from_current_maximal_set(const UnfoldingEvent* e) { current_maximal_set.remove(e); bookkeeper.mark_removed_from_maximal_set(e); @@ -79,18 +86,10 @@ maximal_subsets_iterator::topological_order_position maximal_subsets_iterator::bookkeeper::find_next_event(topological_order_position first, topological_order_position last) const { - return std::find_if(first, last, [&](UnfoldingEvent* e) { return is_candidate_event(e); }); -} - -bool maximal_subsets_iterator::bookkeeper::is_candidate_event(UnfoldingEvent* e) const -{ - if (const auto e_count = event_counts.find(e); e_count != event_counts.end()) { - return e_count->second == 0; - } - return true; + return std::find_if(first, last, [&](const UnfoldingEvent* e) { return is_candidate_event(e); }); } -void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(UnfoldingEvent* e) +void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(const UnfoldingEvent* e) { const auto e_history = e->get_history(); for (const auto e_hist : e_history) { @@ -98,7 +97,7 @@ void maximal_subsets_iterator::bookkeeper::mark_included_in_maximal_set(Unfoldin } } -void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(UnfoldingEvent* e) +void maximal_subsets_iterator::bookkeeper::mark_removed_from_maximal_set(const UnfoldingEvent* e) { const auto e_history = e->get_history(); for (const auto e_hist : e_history) { diff --git a/src/mc/explo/udpor/maximal_subsets_iterator.hpp b/src/mc/explo/udpor/maximal_subsets_iterator.hpp index b51144ec09..79eabb7141 100644 --- a/src/mc/explo/udpor/maximal_subsets_iterator.hpp +++ b/src/mc/explo/udpor/maximal_subsets_iterator.hpp @@ -57,9 +57,9 @@ public: } private: - using topological_order_position = std::vector::const_iterator; + using topological_order_position = std::vector::const_iterator; const std::optional> config; - const std::vector topological_ordering; + const std::vector topological_ordering; const std::optional filter; EventSet current_maximal_set = EventSet(); @@ -78,19 +78,19 @@ private: struct bookkeeper { private: using topological_order_position = maximal_subsets_iterator::topological_order_position; - std::unordered_map event_counts; + std::unordered_map event_counts; - bool is_candidate_event(UnfoldingEvent*) const; + bool is_candidate_event(const UnfoldingEvent*) const; public: - void mark_included_in_maximal_set(UnfoldingEvent*); - void mark_removed_from_maximal_set(UnfoldingEvent*); + void mark_included_in_maximal_set(const UnfoldingEvent*); + void mark_removed_from_maximal_set(const UnfoldingEvent*); topological_order_position find_next_event(topological_order_position first, topological_order_position last) const; } bookkeeper; - void add_element_to_current_maximal_set(UnfoldingEvent*); - void remove_element_from_current_maximal_set(UnfoldingEvent*); + void add_element_to_current_maximal_set(const UnfoldingEvent*); + void remove_element_from_current_maximal_set(const UnfoldingEvent*); // boost::iterator_facade<...> interface to implement void increment();