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 8a298fb..02452aa 100644 (file)
--- 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<EventSet, EventSet> UdporChecker::compute_extension(const Configurati
   //
   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
   //    U{<a, K> : 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<State> 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 30407c4..5e0b575 100644 (file)
--- 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 a05d3a7..70f4659 100644 (file)
--- 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<UnfoldingEvent*> events) : Configuration(EventSet(std::move(events)))
+Configuration::Configuration(std::initializer_list<const UnfoldingEvent*> 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<UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
+std::vector<const UnfoldingEvent*> Configuration::get_topologically_sorted_events() const
 {
   if (events_.empty()) {
-    return std::vector<UnfoldingEvent*>();
+    return std::vector<const UnfoldingEvent*>();
   }
 
-  std::stack<UnfoldingEvent*> event_stack;
-  std::vector<UnfoldingEvent*> topological_ordering;
+  std::stack<const UnfoldingEvent*> event_stack;
+  std::vector<const UnfoldingEvent*> topological_ordering;
   EventSet unknown_events = events_;
   EventSet temporarily_marked_events;
   EventSet permanently_marked_events;
@@ -63,7 +64,7 @@ std::vector<UnfoldingEvent*> 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<UnfoldingEvent*> Configuration::get_topologically_sorted_events() co
   return topological_ordering;
 }
 
-std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events_of_reverse_graph() const
+std::vector<const UnfoldingEvent*> 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 8b2c219..a820a41 100644 (file)
--- 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 <boost/iterator/iterator_facade.hpp>
 #include <functional>
 #include <initializer_list>
+#include <optional>
 #include <vector>
 
 namespace simgrid::mc::udpor {
@@ -23,14 +25,14 @@ public:
   Configuration(Configuration&&)                 = default;
 
   explicit Configuration(const EventSet& events);
-  explicit Configuration(std::initializer_list<UnfoldingEvent*> events);
+  explicit Configuration(std::initializer_list<const UnfoldingEvent*> 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<UnfoldingEvent*> get_topologically_sorted_events() const;
+  std::vector<const UnfoldingEvent*> 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<UnfoldingEvent*> get_topologically_sorted_events_of_reverse_graph() const;
+  std::vector<const UnfoldingEvent*> 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 f9d025e..fdfc914 100644 (file)
--- 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<UnfoldingEvent*>{&e1, &e2, &e3, &e4});
-    REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e4, &e3, &e2, &e1});
+    REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
+    REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+            std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
     }
 
     SECTION("e1 only")
     {
       Configuration C{&e1};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
     }
 
     SECTION("e1 and e2 only")
     {
       Configuration C{&e1, &e2};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
     }
 
     SECTION("e1, e2, and e3 only")
     {
       Configuration C{&e1, &e2, &e3};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e3, &e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+              std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
     }
 
     SECTION("e1 only")
     {
       Configuration C{&e1};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
     }
 
     SECTION("e1 and e2 only")
     {
       Configuration C{&e1, &e2};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
     }
 
     SECTION("e1, e2, and e3 only")
     {
       Configuration C{&e1, &e2, &e3};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e3, &e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+              std::vector<const UnfoldingEvent*>{&e3, &e2, &e1});
     }
 
     SECTION("e1, e2, e3, and e6 only")
     {
       Configuration C{&e1, &e2, &e3, &e6};
-      REQUIRE(C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e6, &e3, &e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+              std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{&e1, &e2, &e3, &e4});
-      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<UnfoldingEvent*>{&e4, &e3, &e2, &e1});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
+      REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
+              std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5});
+      REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5});
       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
-              std::vector<UnfoldingEvent*>{&e5, &e4, &e3, &e2, &e1});
+              std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6} ||
-               C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4}));
+      REQUIRE((C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6} ||
+               C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4}));
       REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
-                   std::vector<UnfoldingEvent*>{&e6, &e4, &e3, &e2, &e1} ||
+                   std::vector<const UnfoldingEvent*>{&e6, &e4, &e3, &e2, &e1} ||
                C.get_topologically_sorted_events_of_reverse_graph() ==
-                   std::vector<UnfoldingEvent*>{&e4, &e6, &e3, &e2, &e1}));
+                   std::vector<const UnfoldingEvent*>{&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<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5, &e6} ||
-               C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6, &e5} ||
-               C.get_topologically_sorted_events() == std::vector<UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4, &e5}));
+      REQUIRE(
+          (C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5, &e6} ||
+           C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6, &e5} ||
+           C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4, &e5}));
       REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
-                   std::vector<UnfoldingEvent*>{&e6, &e5, &e4, &e3, &e2, &e1} ||
+                   std::vector<const UnfoldingEvent*>{&e6, &e5, &e4, &e3, &e2, &e1} ||
                C.get_topologically_sorted_events_of_reverse_graph() ==
-                   std::vector<UnfoldingEvent*>{&e5, &e6, &e4, &e3, &e2, &e1} ||
+                   std::vector<const UnfoldingEvent*>{&e5, &e6, &e4, &e3, &e2, &e1} ||
                C.get_topologically_sorted_events_of_reverse_graph() ==
-                   std::vector<UnfoldingEvent*>{&e5, &e4, &e6, &e3, &e2, &e1}));
+                   std::vector<const UnfoldingEvent*>{&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 c0f0195..5417103 100644 (file)
--- 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<UnfoldingEvent*> result = this->events_;
+  std::unordered_set<const UnfoldingEvent*> 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<UnfoldingEvent*> result = this->events_;
+  std::unordered_set<const UnfoldingEvent*> 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 26a910a..4c64746 100644 (file)
--- 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<UnfoldingEvent*> events_;
+  std::unordered_set<const UnfoldingEvent*> 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<UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
-  explicit EventSet(std::initializer_list<UnfoldingEvent*> event_list) : events_(std::move(event_list)) {}
+  explicit EventSet(std::unordered_set<const UnfoldingEvent*>&& raw_events) : events_(raw_events) {}
+  explicit EventSet(std::initializer_list<const UnfoldingEvent*> 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 313b464..d9d43d3 100644 (file)
--- 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 2deb655..da35244 100644 (file)
--- 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<Iterator, UnfoldingEvent* const, boost::forward_traversal_tag> {
+  struct Iterator : boost::iterator_facade<Iterator, const UnfoldingEvent* const, boost::forward_traversal_tag> {
   public:
     using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
     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 5ca2229..88f4b82 100644 (file)
--- 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<UnfoldingEvent*> init_list)
+UnfoldingEvent::UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> 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 edd7eec..f19c41e 100644 (file)
--- 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<UnfoldingEvent*> init_list);
+  explicit UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list);
   UnfoldingEvent(EventSet immediate_causes              = EventSet(),
                  std::shared_ptr<Transition> transition = std::make_unique<Transition>());
 
@@ -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 a96287d..a811401 100644 (file)
--- 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 b51144e..79eabb7 100644 (file)
--- 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<UnfoldingEvent*>::const_iterator;
+  using topological_order_position = std::vector<const UnfoldingEvent*>::const_iterator;
   const std::optional<std::reference_wrapper<const Configuration>> config;
-  const std::vector<UnfoldingEvent*> topological_ordering;
+  const std::vector<const UnfoldingEvent*> topological_ordering;
   const std::optional<node_filter_function> 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<UnfoldingEvent*, unsigned> event_counts;
+    std::unordered_map<const UnfoldingEvent*, unsigned> 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();