From: Augustin Degomme <26892-adegomme@users.noreply.framagit.org>
Date: Tue, 28 Feb 2023 15:59:29 +0000 (+0000)
Subject: Merge branch 'udpor-phase3' into 'master'
X-Git-Tag: v3.34~422
X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b6a2ada11480242c200660a273f4174151d0bf09?hp=0d81597680da4b8a8adc651ecc611aa2c6e001ff

Merge branch 'udpor-phase3' into 'master'

Phase 2.5 of UDPOR Integration: Add Iterators for Subsets

See merge request simgrid/simgrid!134
---

diff --git a/MANIFEST.in b/MANIFEST.in
index b77754eb8e..65044786f6 100644
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2234,6 +2234,16 @@ include src/mc/transition/TransitionRandom.cpp
 include src/mc/transition/TransitionRandom.hpp
 include src/mc/transition/TransitionSynchro.cpp
 include src/mc/transition/TransitionSynchro.hpp
+include src/mc/explo/udpor/Configuration.hpp
+include src/mc/explo/udpor/Configuration.cpp
+include src/mc/explo/udpor/EventSet.cpp
+include src/mc/explo/udpor/EventSet.hpp
+include src/mc/explo/udpor/History.cpp
+include src/mc/explo/udpor/History.hpp
+include src/mc/explo/udpor/UnfoldingEvent.cpp
+include src/mc/explo/udpor/UnfoldingEvent.hpp
+include src/mc/explo/udpor/Unfolding.cpp
+include src/mc/explo/udpor/Unfolding.hpp
 include src/plugins/ProducerConsumer.cpp
 include src/plugins/chaos_monkey.cpp
 include src/plugins/file_system/s4u_FileSystem.cpp
@@ -2508,6 +2518,11 @@ include src/xbt/random_test.cpp
 include src/xbt/snprintf.c
 include src/xbt/string.cpp
 include src/xbt/unit-tests_main.cpp
+include src/xbt/utils/iter/subsets.hpp
+include src/xbt/utils/iter/subsets_tests.cpp
+include src/xbt/utils/iter/powerset.hpp
+include src/xbt/utils/iter/LazyKSubsets.hpp
+include src/xbt/utils/iter/LazyPowerset.hpp
 include src/xbt/xbt_log_appender_file.cpp
 include src/xbt/xbt_log_layout_format.cpp
 include src/xbt/xbt_log_layout_simple.cpp
diff --git a/src/mc/api/ActorState.hpp b/src/mc/api/ActorState.hpp
index eda280894b..946971af29 100644
--- a/src/mc/api/ActorState.hpp
+++ b/src/mc/api/ActorState.hpp
@@ -131,6 +131,11 @@ public:
                aid_, times_considered);
     this->pending_transitions_[times_considered] = std::move(t);
   }
+
+  const std::vector<std::shared_ptr<Transition>>& get_enabled_transitions() const
+  {
+    return this->pending_transitions_;
+  };
 };
 
 } // namespace simgrid::mc
diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index ff61f17a39..8a298fbc5a 100644
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -14,9 +14,7 @@ namespace simgrid::mc::udpor {
 
 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
 {
-  /* Create initial data structures, if any ...*/
-
-  // TODO: Initialize state structures for the search
+  // Initialize the map
 }
 
 void UdporChecker::run()
@@ -34,12 +32,13 @@ void UdporChecker::run()
   unfolding.insert(std::move(root_event));
   C_root.add_event(root_event_handle);
 
-  explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet());
+  explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
 
   XBT_INFO("UDPOR exploration terminated -- model checking completed");
 }
 
-void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
+void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
+                           EventSet prev_exC)
 {
   // Perform the incremental computation of exC
   //
@@ -47,7 +46,7 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
   // the unfolding, but the naming of the method
   // suggests it is doesn't have side effects. We should
   // reconcile this in the future
-  auto [exC, enC] = compute_extension(C, prev_exC);
+  auto [exC, enC] = compute_extension(C, *stateC, prev_exC);
 
   // If enC is a subset of D, intuitively
   // there aren't any enabled transitions
@@ -56,14 +55,8 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
   // "sleep-set blocked" trace.
   if (enC.is_subset_of(D)) {
 
-    if (C.get_events().size() > 0) {
-
-      // g_var::nb_traces++;
-
-      // TODO: Log here correctly
-      // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
-      // ...
-      // ...
+    if (not C.get_events().empty()) {
+      // Report information...
     }
 
     // When `en(C)` is empty, intuitively this means that there
@@ -105,8 +98,7 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
 
   // TODO: Determine a value of K to use or don't use it at all
   constexpr unsigned K = 10;
-  auto J               = compute_partial_alternative(D, C, K);
-  if (!J.empty()) {
+  if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
     J.subtract(C.get_events());
 
     // Before searching the "right half", we need to make
@@ -126,24 +118,54 @@ void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_
   clean_up_explore(e, C, D);
 }
 
-std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const
+std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const State& stateC,
+                                                               const EventSet& prev_exC) const
 {
   // See eqs. 5.7 of section 5.2 of [3]
   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
   //
   // Then
   //
-  // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
+  // 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;
   exC.remove(e_cur);
 
-  // ... fancy computations
+  for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
+    for (const auto& transition : actor_state.get_enabled_transitions()) {
+      // First check for a specialized function that can compute the extension
+      // set "quickly" based on its type. Otherwise, fall back to computing
+      // the set "by hand"
+      const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
+      if (specialized_extension_function != incremental_extension_functions.end()) {
+        exC.form_union((specialized_extension_function->second)(C, *transition));
+      } else {
+        exC.form_union(this->compute_extension_by_enumeration(C, *transition));
+      }
+    }
+  }
 
   EventSet enC;
+  // TODO: Compute enC based on conflict relations
+
   return std::tuple<EventSet, EventSet>(exC, enC);
 }
 
+EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
+{
+  // Here we're computing the following:
+  //
+  // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
+  //
+  // where `a` is the `action` given to us.
+  EventSet incremental_exC;
+
+  // Compute the extension set here using the algorithm Martin described...
+
+  return incremental_exC;
+}
+
 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 {
   const aid_t next_actor = e.get_transition()->aid_;
diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index 7f56d6d3d5..30407c4217 100644
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -14,6 +14,7 @@
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/mc_record.hpp"
 
+#include <functional>
 #include <optional>
 
 namespace simgrid::mc::udpor {
@@ -41,14 +42,6 @@ public:
   inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
 
 private:
-  /**
-   * The total number of events created whilst exploring the unfolding
-   */
-  /* FIXME: private fields are not used
-    uint32_t nb_events = 0;
-    uint32_t nb_traces = 0;
-  */
-
   /**
    * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
    * UDPOR properly searches the state space
@@ -75,12 +68,18 @@ private:
    */
   EventSet G;
 
+  /// @brief UDPOR's current "view" of the program it is exploring
+  Unfolding unfolding = Unfolding();
+
+  using ExtensionFunction = std::function<EventSet(const Configuration&, const Transition&)>;
+
   /**
-   * @brief UDPOR's current "view" of the program it is exploring
+   * @brief A collection of specialized functions which can incrementally
+   * compute the extension of a configuration based on the action taken
    */
-  Unfolding unfolding = Unfolding();
+  std::unordered_map<Transition::Type, ExtensionFunction> incremental_extension_functions =
+      std::unordered_map<Transition::Type, ExtensionFunction>();
 
-private:
   /**
    * @brief Explores the unfolding of the concurrent system
    * represented by the ModelChecker instance "mcmodel_checker"
@@ -102,7 +101,7 @@ private:
    * TODO: Add the optimization where we can check if e == e_prior
    * to prevent repeated work when computing ex(C)
    */
-  void explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
+  void explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC);
 
   /**
    * @brief Identifies the next event from the unfolding of the concurrent system
@@ -137,11 +136,15 @@ private:
    *
    * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
    * computed
+   * @param stateC the state of the program after having executed C (viz. `state(C)`)
    * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
    * the configuration `C' := C - {e}`
    * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
    */
-  std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const EventSet& prev_exC) const;
+  std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const State& stateC,
+                                                   const EventSet& prev_exC) const;
+
+  EventSet compute_extension_by_enumeration(const Configuration& C, const Transition& action) const;
 
   /**
    *
diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp
index 8fa1dd6285..a05d3a7a0a 100644
--- a/src/mc/explo/udpor/Configuration.cpp
+++ b/src/mc/explo/udpor/Configuration.cpp
@@ -6,6 +6,7 @@
 #include "src/mc/explo/udpor/Configuration.hpp"
 #include "src/mc/explo/udpor/History.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "xbt/asserts.h"
 
 #include <algorithm>
 #include <stack>
@@ -17,7 +18,7 @@ Configuration::Configuration(std::initializer_list<UnfoldingEvent*> events) : Co
 {
 }
 
-Configuration::Configuration(EventSet events) : events_(events)
+Configuration::Configuration(const EventSet& events) : events_(events)
 {
   if (!events_.is_valid_configuration()) {
     throw std::invalid_argument("The events do not form a valid configuration");
@@ -53,7 +54,9 @@ std::vector<UnfoldingEvent*> Configuration::get_topologically_sorted_events() co
 
   std::stack<UnfoldingEvent*> event_stack;
   std::vector<UnfoldingEvent*> topological_ordering;
-  EventSet unknown_events = events_, temporarily_marked_events, permanently_marked_events;
+  EventSet unknown_events = events_;
+  EventSet temporarily_marked_events;
+  EventSet permanently_marked_events;
 
   while (not unknown_events.empty()) {
     EventSet discovered_events;
diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index 1ccb9e8dd9..8b2c219df6 100644
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -9,6 +9,7 @@
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/udpor_forward.hpp"
 
+#include <functional>
 #include <initializer_list>
 #include <vector>
 
@@ -21,8 +22,8 @@ public:
   Configuration& operator=(Configuration const&) = default;
   Configuration(Configuration&&)                 = default;
 
-  Configuration(EventSet events);
-  Configuration(std::initializer_list<UnfoldingEvent*> events);
+  explicit Configuration(const EventSet& events);
+  explicit Configuration(std::initializer_list<UnfoldingEvent*> events);
 
   auto begin() const { return this->events_.begin(); }
   auto end() const { return this->events_.end(); }
diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp
index bf12e98765..9a5a756b08 100644
--- a/src/mc/explo/udpor/Configuration_test.cpp
+++ b/src/mc/explo/udpor/Configuration_test.cpp
@@ -24,7 +24,8 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
   UnfoldingEvent e1;
   UnfoldingEvent e2{&e1};
   UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3}, e5{&e3};
+  UnfoldingEvent e4{&e3};
+  UnfoldingEvent e5{&e3};
 
   SECTION("Creating a configuration without events")
   {
@@ -191,8 +192,9 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli
   UnfoldingEvent e1;
   UnfoldingEvent e2{&e1};
   UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3}, e6{&e3};
+  UnfoldingEvent e4{&e3};
   UnfoldingEvent e5{&e4};
+  UnfoldingEvent e6{&e3};
 
   SECTION("Topological ordering for subsets")
   {
@@ -293,26 +295,28 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli
   //         /  /   /
   //         [   e12    ]
   UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1}, e8{&e1};
+  UnfoldingEvent e2{&e1};
+  UnfoldingEvent e8{&e1};
   UnfoldingEvent e3{&e2};
   UnfoldingEvent e4{&e3};
-  UnfoldingEvent e5{&e4}, e6{&e4};
-  UnfoldingEvent e7{&e2, &e8}, e11{&e8};
-  UnfoldingEvent e10{&e7}, e9{&e6, &e7};
+  UnfoldingEvent e5{&e4};
+  UnfoldingEvent e6{&e4};
+  UnfoldingEvent e7{&e2, &e8};
+  UnfoldingEvent e9{&e6, &e7};
+  UnfoldingEvent e10{&e7};
+  UnfoldingEvent e11{&e8};
   UnfoldingEvent e12{&e5, &e9, &e10};
+  Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
 
   SECTION("Test every combination of the maximal configuration (forward graph)")
   {
     // To test this, we ensure that for the `i`th event
     // in `ordered_events`, each event in `ordered_events[0...<i]
     // is contained in the history of `ordered_events[i]`.
-    Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
-    const auto ordered_events = C.get_topologically_sorted_events();
-
     EventSet events_seen;
-    for (size_t i = 0; i < ordered_events.size(); i++) {
-      UnfoldingEvent* e = ordered_events[i];
+    const auto ordered_events = C.get_topologically_sorted_events();
 
+    std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
       History history(e);
       for (auto* e_hist : history) {
         // In this demo, we want to make sure that
@@ -328,7 +332,7 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli
         REQUIRE(events_seen.contains(e_hist));
       }
       events_seen.insert(e);
-    }
+    });
   }
 
   SECTION("Test every combination of the maximal configuration (reverse graph)")
@@ -336,12 +340,10 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli
     // To test this, we ensure that for the `i`th event
     // in `ordered_events`, no event in `ordered_events[0...<i]
     // is contained in the history of `ordered_events[i]`.
-    Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
+    EventSet events_seen;
     const auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
 
-    EventSet events_seen;
-    for (size_t i = 0; i < ordered_events.size(); i++) {
-      UnfoldingEvent* e = ordered_events[i];
+    std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](UnfoldingEvent* e) {
       History history(e);
 
       for (auto* e_hist : history) {
@@ -354,6 +356,6 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli
         REQUIRE_FALSE(events_seen.contains(e_hist));
       }
       events_seen.insert(e);
-    }
+    });
   }
 }
\ No newline at end of file
diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index 6f486b7732..b03bef5933 100644
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -11,7 +11,7 @@
 
 namespace simgrid::mc::udpor {
 
-EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {}
+EventSet::EventSet(Configuration&& config) : EventSet(config.get_events()) {}
 
 void EventSet::remove(UnfoldingEvent* e)
 {
diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index e640f0c9de..26a910a7d6 100644
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -56,7 +56,6 @@ public:
   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
   bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }
 
-public:
   /**
    * @brief Whether or not this set of events could
    * represent a configuration
diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp
index 77a555d2f4..d7342b39a6 100644
--- a/src/mc/explo/udpor/EventSet_test.cpp
+++ b/src/mc/explo/udpor/EventSet_test.cpp
@@ -51,7 +51,6 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets")
 
     SECTION("List initialization")
     {
-      UnfoldingEvent e1, e2, e3;
       EventSet event_set{&e1, &e2, &e3};
       REQUIRE(event_set.size() == 3);
       REQUIRE(event_set.contains(&e1));
@@ -110,14 +109,17 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Insertions")
 
 TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
 {
-  UnfoldingEvent e1, e2, e3, e4;
+  UnfoldingEvent e1;
+  UnfoldingEvent e2;
+  UnfoldingEvent e3;
+  UnfoldingEvent e4;
   EventSet event_set({&e1, &e2, &e3});
 
   SECTION("Remove an element already present")
   {
     REQUIRE(event_set.contains(&e1));
 
-    // event_set = {e2, e3}
+    // Recall that event_set = {e2, e3}
     event_set.remove(&e1);
 
     // Check that
@@ -132,7 +134,7 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
 
     SECTION("Remove a single element more than once")
     {
-      // event_set = {e2, e3}
+      // Recall that event_set = {e2, e3}
       event_set.remove(&e1);
       REQUIRE(event_set.size() == 2);
       REQUIRE_FALSE(event_set.contains(&e1));
@@ -143,7 +145,7 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
 
     SECTION("Remove more than one element")
     {
-      // event_set = {e3}
+      // Recall that event_set = {e3}
       event_set.remove(&e2);
 
       REQUIRE(event_set.size() == 1);
@@ -152,7 +154,7 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
       REQUIRE(event_set.contains(&e3));
       REQUIRE_FALSE(event_set.empty());
 
-      // event_set = {}
+      // Recall that event_set = {}
       event_set.remove(&e3);
 
       REQUIRE(event_set.size() == 0);
@@ -167,7 +169,7 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
   {
     REQUIRE_FALSE(event_set.contains(&e4));
 
-    // event_set = {e1, e2, e3}
+    // Recall that event_set = {e1, e2, e3}
     event_set.remove(&e4);
     REQUIRE(event_set.size() == 3);
     REQUIRE(event_set.contains(&e1));
@@ -182,7 +184,10 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
 
 TEST_CASE("simgrid::mc::udpor::EventSet: Set Equality")
 {
-  UnfoldingEvent e1, e2, e3, e4;
+  UnfoldingEvent e1;
+  UnfoldingEvent e2;
+  UnfoldingEvent e3;
+  UnfoldingEvent e4;
   EventSet A{&e1, &e2, &e3}, B{&e1, &e2, &e3}, C{&e1, &e2, &e3};
 
   SECTION("Equality implies containment")
@@ -516,8 +521,10 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Testing Configurations")
   // in the structure and test whether those subsets are
   // maximal and/or valid configurations
   UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1}, e5{&e1};
-  UnfoldingEvent e3{&e2}, e4{&e2};
+  UnfoldingEvent e2{&e1};
+  UnfoldingEvent e3{&e2};
+  UnfoldingEvent e4{&e2};
+  UnfoldingEvent e5{&e1};
   UnfoldingEvent e6{&e5};
 
   SECTION("Valid Configurations")
diff --git a/src/mc/explo/udpor/History.cpp b/src/mc/explo/udpor/History.cpp
index 544980a8cf..e6a6405f9e 100644
--- a/src/mc/explo/udpor/History.cpp
+++ b/src/mc/explo/udpor/History.cpp
@@ -45,7 +45,7 @@ History::Iterator& History::Iterator::operator++()
     maximal_events.subtract(candidates);
 
     candidates.subtract(current_history);
-    frontier.form_union(std::move(candidates));
+    frontier.form_union(candidates);
   }
   return *this;
 }
@@ -72,15 +72,15 @@ EventSet History::get_all_maximal_events() const
   return first.maximal_events;
 }
 
-bool History::contains(UnfoldingEvent* e) const
+bool History::contains(const UnfoldingEvent* e) const
 {
-  return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });
+  return std::any_of(this->begin(), this->end(), [=](const UnfoldingEvent* e_hist) { return e == e_hist; });
 }
 
 EventSet History::get_event_diff_with(const Configuration& config) const
 {
   auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
-  auto first          = Iterator(events_, std::move(wrapped_config));
+  auto first          = Iterator(events_, wrapped_config);
   const auto last     = this->end();
 
   for (; first != last; ++first)
diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp
index e667424175..7087927801 100644
--- a/src/mc/explo/udpor/History.hpp
+++ b/src/mc/explo/udpor/History.hpp
@@ -71,7 +71,7 @@ public:
    * @param e the event to check
    * @returns whether or not `e` is contained in the collection
    */
-  bool contains(UnfoldingEvent* e) const;
+  bool contains(const UnfoldingEvent* e) const;
 
   /**
    * @brief Computes all events in the history described by this instance
@@ -102,14 +102,14 @@ private:
   struct Iterator {
   public:
     Iterator& operator++();
-    auto operator->() { return frontier.begin().operator->(); }
+    auto operator->() const { return frontier.begin().operator->(); }
     auto operator*() const { return *frontier.begin(); }
 
     // If what the iterator sees next is the same, we consider them
     // to be the same iterator. This way, once the iterator has completed
     // its search, it will be "equal" to an iterator searching nothing
-    bool operator==(const Iterator& other) { return this->frontier == other.frontier; }
-    bool operator!=(const Iterator& other) { return not(this->operator==(other)); }
+    bool operator==(const Iterator& other) const { return this->frontier == other.frontier; }
+    bool operator!=(const Iterator& other) const { return not(this->operator==(other)); }
 
     using iterator_category      = std::forward_iterator_tag;
     using difference_type        = int; // # of steps between
diff --git a/src/mc/explo/udpor/History_test.cpp b/src/mc/explo/udpor/History_test.cpp
index 0cbe87881a..55065a3e91 100644
--- a/src/mc/explo/udpor/History_test.cpp
+++ b/src/mc/explo/udpor/History_test.cpp
@@ -18,9 +18,12 @@ TEST_CASE("simgrid::mc::udpor::History: History generation")
   //  | \  \  /   /
   // e3 e4 e5      e7
   UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1}, e6{&e1};
-  UnfoldingEvent e3{&e2}, e4{&e2};
-  UnfoldingEvent e5{&e2, &e6}, e7{&e6};
+  UnfoldingEvent e2{&e1};
+  UnfoldingEvent e6{&e1};
+  UnfoldingEvent e3{&e2};
+  UnfoldingEvent e4{&e2};
+  UnfoldingEvent e5{&e2, &e6};
+  UnfoldingEvent e7{&e6};
 
   SECTION("History with no events")
   {
diff --git a/src/mc/explo/udpor/UnfoldingEvent.hpp b/src/mc/explo/udpor/UnfoldingEvent.hpp
index 2bd29e991b..4468b210c5 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:
-  UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
+  explicit UnfoldingEvent(std::initializer_list<UnfoldingEvent*> init_list);
   UnfoldingEvent(EventSet immediate_causes              = EventSet(),
                  std::shared_ptr<Transition> transition = std::make_unique<Transition>());
 
@@ -38,7 +38,6 @@ public:
 
   bool operator==(const UnfoldingEvent&) const;
 
-private:
   /**
    * @brief The transition that UDPOR "attaches" to this
    * specific event for later use while computing e.g. extension
diff --git a/src/xbt/utils/iter/LazyKSubsets.hpp b/src/xbt/utils/iter/LazyKSubsets.hpp
new file mode 100644
index 0000000000..e9773d1582
--- /dev/null
+++ b/src/xbt/utils/iter/LazyKSubsets.hpp
@@ -0,0 +1,52 @@
+/* Copyright (c) 2004-2023 The SimGrid Team. All rights reserved.           */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef XBT_UTILS_LAZY_KSUBSETS_HPP
+#define XBT_UTILS_LAZY_KSUBSETS_HPP
+
+#include "src/xbt/utils/iter/subsets.hpp"
+
+namespace simgrid::xbt {
+
+template <class Iterable> class LazyKSubsets;
+template <class Iterable> LazyKSubsets<Iterable> make_k_subsets_iter(unsigned k, const Iterable& container);
+
+/**
+ * @brief A container which "contains" all subsets of
+ * size `k` of some other container `WrapperContainer`
+ *
+ * @note: You should not store instances of this class directly,
+ * as it acts more like a simply wrapping around another iterable
+ * type to make it more convenient to iterate over subsets of
+ * some iterable type.
+ *
+ * @class Iterable: The container from which
+ * the subsets "contained" by this container are derived
+ */
+template <class Iterable> class LazyKSubsets final {
+public:
+  auto begin() const
+  {
+    return subsets_iterator<typename Iterable::const_iterator>(k, iterable.begin(), iterable.end());
+  }
+  auto end() const { return subsets_iterator<typename Iterable::const_iterator>(k); }
+
+private:
+  const unsigned k;
+  const Iterable& iterable;
+  LazyKSubsets(unsigned k, const Iterable& iterable) : k(k), iterable(iterable) {}
+
+  template <class IterableType>
+  friend LazyKSubsets<IterableType> make_k_subsets_iter(unsigned k, const IterableType& iterable);
+};
+
+template <class Iterable> LazyKSubsets<Iterable> make_k_subsets_iter(unsigned k, const Iterable& container)
+{
+  return LazyKSubsets<Iterable>(k, container);
+}
+
+} // namespace simgrid::xbt
+
+#endif
diff --git a/src/xbt/utils/iter/LazyPowerset.hpp b/src/xbt/utils/iter/LazyPowerset.hpp
new file mode 100644
index 0000000000..76d348353d
--- /dev/null
+++ b/src/xbt/utils/iter/LazyPowerset.hpp
@@ -0,0 +1,46 @@
+/* Copyright (c) 2004-2023 The SimGrid Team. All rights reserved.           */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef XBT_UTILS_LAZY_POWER_SET_HPP
+#define XBT_UTILS_LAZY_POWER_SET_HPP
+
+#include "src/xbt/utils/iter/powerset.hpp"
+
+namespace simgrid::xbt {
+
+template <class Iterable> class LazyPowerset;
+template <class Iterable> LazyPowerset<Iterable> make_powerset_iter(const Iterable& container);
+
+/**
+ * @brief A container which "contains" all subsets of
+ * size `k` of some other container `WrapperContainer`
+ *
+ * @note: You should not store instances of this class directly,
+ * as it acts more like a simply wrapping around another iterable
+ * type to make it more convenient to iterate over subsets of
+ * some iterable type.
+ *
+ * @class Iterable: The container from which
+ * the subsets "contained" by this container are derived
+ */
+template <class Iterable> class LazyPowerset final {
+public:
+  auto begin() const { return powerset_iterator<typename Iterable::const_iterator>(iterable.begin(), iterable.end()); }
+  auto end() const { return powerset_iterator<typename Iterable::const_iterator>(); }
+
+private:
+  const Iterable& iterable;
+  LazyPowerset(const Iterable& iterable) : iterable(iterable) {}
+  template <class IterableType> friend LazyPowerset<IterableType> make_powerset_iter(const IterableType& iterable);
+};
+
+template <class Iterable> LazyPowerset<Iterable> make_powerset_iter(const Iterable& container)
+{
+  return LazyPowerset<Iterable>(container);
+}
+
+} // namespace simgrid::xbt
+
+#endif
diff --git a/src/xbt/utils/iter/powerset.hpp b/src/xbt/utils/iter/powerset.hpp
new file mode 100644
index 0000000000..0f477236ab
--- /dev/null
+++ b/src/xbt/utils/iter/powerset.hpp
@@ -0,0 +1,105 @@
+/* Copyright (c) 2004-2023 The SimGrid Team. All rights reserved.           */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef XBT_UTILS_ITER_POWERSET_HPP
+#define XBT_UTILS_ITER_POWERSET_HPP
+
+#include "src/xbt/utils/iter/subsets.hpp"
+
+#include <boost/iterator/iterator_facade.hpp>
+#include <optional>
+
+namespace simgrid::xbt {
+
+/**
+ * @brief A higher-order iterator which traverses all possible subsets
+ * of the elements of an iterable sequence.
+ *
+ * @note The power set `P(S)` of any finite set `S` is of exponential size relative
+ * to the size of `S`. Be warned that attempting to iterate over the power set of
+ * large sets will cost a LOT of time (but that the memory footprint will remain
+ * very small). Alas, unless P = NP, there sometimes isn't a better known way to
+ * solve a problem (e.g. determining all cliques in a graph)
+ *
+ * @class Iterator: The iterator over which this higher-order iterator
+ * generates elements
+ */
+template <class Iterator>
+struct powerset_iterator : public boost::iterator_facade<powerset_iterator<Iterator>, const std::vector<Iterator>,
+                                                         boost::forward_traversal_tag> {
+  powerset_iterator() = default;
+  explicit powerset_iterator(Iterator begin, Iterator end = Iterator());
+
+private:
+  // The current size of the subsets
+  unsigned n = 0;
+  std::optional<Iterator> iterator_begin;
+  std::optional<Iterator> iterator_end;
+  std::optional<subsets_iterator<Iterator>> current_subset_iter     = std::nullopt;
+  std::optional<subsets_iterator<Iterator>> current_subset_iter_end = std::nullopt;
+
+  const std::vector<Iterator> empty_subset = std::vector<Iterator>();
+
+  // boost::iterator_facade<...> interface to implement
+  void increment();
+  bool equal(const powerset_iterator<Iterator>& other) const;
+  const std::vector<Iterator>& dereference() const;
+
+  // Allows boost::iterator_facade<...> to function properly
+  friend class boost::iterator_core_access;
+};
+
+template <typename Iterator>
+powerset_iterator<Iterator>::powerset_iterator(Iterator begin, Iterator end)
+    : iterator_begin({begin})
+    , iterator_end({end})
+    , current_subset_iter({subsets_iterator<Iterator>(0, begin, end)})
+    , current_subset_iter_end({subsets_iterator<Iterator>(0)})
+{
+}
+
+template <typename Iterator> bool powerset_iterator<Iterator>::equal(const powerset_iterator<Iterator>& other) const
+{
+  return current_subset_iter == other.current_subset_iter;
+}
+
+template <typename Iterator> const std::vector<Iterator>& powerset_iterator<Iterator>::dereference() const
+{
+  if (current_subset_iter.has_value()) {
+    return *current_subset_iter.value();
+  }
+  return empty_subset;
+}
+
+template <typename Iterator> void powerset_iterator<Iterator>::increment()
+{
+  if (!current_subset_iter.has_value() || !current_subset_iter_end.has_value(),
+      !current_subset_iter.has_value() || !iterator_end.has_value()) {
+    return; // We've traversed all subsets at this point, or we're the "last" iterator
+  }
+
+  // Move the underlying subset iterator over
+  ++current_subset_iter.value();
+
+  // If the current underlying subset iterator for size `n`
+  // is finished, generate one for `n = n + 1`
+  if (current_subset_iter == current_subset_iter_end) {
+    n++;
+    current_subset_iter     = {subsets_iterator<Iterator>(n, iterator_begin.value(), iterator_end.value())};
+    current_subset_iter_end = {subsets_iterator<Iterator>(n)};
+
+    // If we've immediately hit a deadend, then we know that the last
+    // value of `n` was the number of elements in the iteration, so
+    // we're done
+    if (current_subset_iter == current_subset_iter_end) {
+      current_subset_iter     = std::nullopt;
+      current_subset_iter_end = std::nullopt;
+    }
+  }
+}
+
+} // namespace simgrid::xbt
+
+#endif
diff --git a/src/xbt/utils/iter/subsets.hpp b/src/xbt/utils/iter/subsets.hpp
new file mode 100644
index 0000000000..1abea21900
--- /dev/null
+++ b/src/xbt/utils/iter/subsets.hpp
@@ -0,0 +1,169 @@
+/* Copyright (c) 2004-2023 The SimGrid Team. All rights reserved.           */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef XBT_UTILS_ITER_SUBSETS_HPP
+#define XBT_UTILS_ITER_SUBSETS_HPP
+
+#include <boost/iterator/iterator_facade.hpp>
+#include <functional>
+#include <numeric>
+#include <optional>
+#include <vector>
+
+namespace simgrid::xbt {
+
+/**
+ * @brief A higher-order forward-iterator which traverses all possible subsets
+ * of a given fixed size `k` of an iterable sequence
+ *
+ * @class Iterator: The iterator over which this higher-order iterator
+ * generates elements.
+ */
+template <class Iterator>
+struct subsets_iterator : public boost::iterator_facade<subsets_iterator<Iterator>, const std::vector<Iterator>,
+                                                        boost::forward_traversal_tag> {
+  subsets_iterator();
+  explicit subsets_iterator(unsigned k);
+  explicit subsets_iterator(unsigned k, Iterator begin, Iterator end = Iterator());
+
+private:
+  unsigned k; // The size of the subsets generated
+  std::optional<Iterator> end = std::nullopt;
+  std::vector<Iterator> current_subset;
+  std::vector<unsigned> P; // Increment counts to determine which combinations need to be traversed
+
+  // boost::iterator_facade<...> interface to implement
+  void increment();
+  bool equal(const subsets_iterator<Iterator>& other) const;
+  const std::vector<Iterator>& dereference() const;
+
+  // Allows boost::iterator_facade<...> to function properly
+  friend class boost::iterator_core_access;
+};
+
+template <typename Iterator> subsets_iterator<Iterator>::subsets_iterator() : subsets_iterator<Iterator>(0) {}
+
+template <typename Iterator>
+subsets_iterator<Iterator>::subsets_iterator(unsigned k)
+    : k(k), current_subset(std::vector<Iterator>(k)), P(std::vector<unsigned>(k))
+{
+  std::iota(P.begin(), P.end(), k);
+}
+
+template <typename Iterator>
+subsets_iterator<Iterator>::subsets_iterator(unsigned k, Iterator begin, Iterator end)
+    : k(k), end(std::optional<Iterator>{end}), current_subset(std::vector<Iterator>(k)), P(std::vector<unsigned>(k))
+{
+  for (unsigned i = 0; i < k; i++) {
+    // Less than `k` elements to choose
+    if (begin == end) {
+      // We want to initialize the object then to be equivalent
+      // to the end iterator so that there are no items to iterate
+      // over
+      this->end = std::nullopt;
+      std::iota(P.begin(), P.end(), k);
+      return;
+    }
+    current_subset[i] = begin++;
+  }
+  std::iota(P.begin(), P.end(), 0);
+}
+
+template <typename Iterator> bool subsets_iterator<Iterator>::equal(const subsets_iterator<Iterator>& other) const
+{
+  if (this->end == std::nullopt and other.end == std::nullopt) {
+    return true;
+  }
+  if (this->k != other.k) {
+    return false;
+  }
+  if (this->k == 0) { // this->k == other.k == 0
+    return true;
+  }
+  return this->end != std::nullopt and other.end != std::nullopt and this->P[0] == other.P[0];
+}
+
+template <typename Iterator> const std::vector<Iterator>& subsets_iterator<Iterator>::dereference() const
+{
+  return this->current_subset;
+}
+
+template <typename Iterator> void subsets_iterator<Iterator>::increment()
+{
+  // If k == 0, there's nothing to do
+  // If end == std::nullopt, we've finished
+  // iterating over all subsets of size `k`
+  if (end == std::nullopt || k == 0) {
+    return;
+  }
+
+  // Move the last element over each time
+  ++current_subset[k - 1];
+  ++P[k - 1];
+
+  const auto end                  = this->end.value();
+  const bool shift_other_elements = current_subset[k - 1] == end;
+
+  if (shift_other_elements) {
+    if (k == 1) {
+      // We're done in the case that k = 1; here, we've iterated
+      // through the list once, which is all that is needed
+      this->end = std::nullopt;
+      return;
+    }
+
+    // At this point, k >= 2
+
+    // The number of elements is now equal to the "index"
+    // of the last element (it is at the end, which means we added
+    // for the last time)
+    const unsigned n = P[k - 1];
+
+    // We're looking to determine
+    //
+    // argmax_{0 <= j <= k - 2}(P[j] != (n - (k - j)))
+    //
+    // If P[j] == (n - (k - j)) for some `j`, that means
+    // the `j`th element of the current subset has moved
+    // "as far as it can move" to the right; in other words,
+    // this is our signal that some element before the `j`th
+    // has to move over
+    //
+    // std::max_element() would work here too, but it seems
+    // overkill to create a vector full of numbers when a simple
+    // range-based for-loop can do the trick
+    unsigned l = 0;
+    for (unsigned j = k - 2; j > 0; j--) {
+      if (P[j] != (n - (k - j))) {
+        l = j;
+        break;
+      }
+    }
+
+    ++P[l];
+    ++current_subset[l];
+
+    // Plugging in `j = 0` to the above formula yields
+    // `n - k`, which is the furthest point that the first (i.e. `0th`)
+    // element can be located. Thus, if `P[0] > (n - k)`, this means
+    // we've sucessfully iterated through all subsets so we're done
+    if (P[0] > (n - k)) {
+      this->end = std::nullopt;
+      return;
+    }
+
+    // Otherwise, all elements past element `l` are reset
+    // to follow one after another immediately after `l`
+    auto iter_at_l = current_subset[l];
+    for (auto i = l + 1; i <= (k - 1); i++) {
+      P[i]              = P[l] + (i - l);
+      current_subset[i] = ++iter_at_l;
+    }
+  }
+}
+
+} // namespace simgrid::xbt
+
+#endif
diff --git a/src/xbt/utils/iter/subsets_tests.cpp b/src/xbt/utils/iter/subsets_tests.cpp
new file mode 100644
index 0000000000..2db7f187ab
--- /dev/null
+++ b/src/xbt/utils/iter/subsets_tests.cpp
@@ -0,0 +1,71 @@
+#include "src/3rd-party/catch.hpp"
+#include "src/xbt/utils/iter/LazyKSubsets.hpp"
+#include "src/xbt/utils/iter/LazyPowerset.hpp"
+
+#include <unordered_map>
+#include <unordered_set>
+#include <vector>
+
+using namespace simgrid::xbt;
+
+// This is used in a number of tests below
+// to verify that counts of elements for example.
+static unsigned integer_power(unsigned x, unsigned p)
+{
+  unsigned i = 1;
+  for (unsigned j = 1; j <= p; j++)
+    i *= x;
+  return i;
+}
+
+TEST_CASE("simgrid::xbt::subsets_iterator: Iteration General Properties")
+{
+  std::vector<int> example_vec{0, 1, 2, 3, 4, 5, 6, 7};
+
+  SECTION("Each element of each subset is distinct and appears half of the time")
+  {
+    for (unsigned k = 0; static_cast<size_t>(k) < example_vec.size(); k++) {
+      for (auto& subset : make_k_subsets_iter(k, example_vec)) {
+        // Each subset must have size `k`
+        REQUIRE(subset.size() == k);
+
+        // Each subset must be comprised only of distinct elements
+        std::unordered_set<int> elements_seen(k);
+        for (const auto& element_ptr : subset) {
+          const auto& element = *element_ptr;
+          REQUIRE(elements_seen.find(element) == elements_seen.end());
+          elements_seen.insert(element);
+        }
+      }
+    }
+  }
+}
+
+TEST_CASE("simgrid::xbt::powerset_iterator: Iteration General Properties")
+{
+  std::vector<int> example_vec{0, 1, 2, 3, 4, 5, 6, 7};
+
+  SECTION("Each element of each subset is distinct and appears half of the time in all subsets iteration")
+  {
+    // Each element is expected to be found in half of the sets
+    const unsigned k         = static_cast<unsigned>(example_vec.size());
+    const int expected_count = integer_power(2, k - 1);
+
+    std::unordered_map<int, int> element_counts(k);
+
+    for (auto& subset : make_powerset_iter(example_vec)) {
+      // Each subset must be comprised only of distinct elements
+      std::unordered_set<int> elements_seen(k);
+      for (const auto& element_ptr : subset) {
+        const auto& element = *element_ptr;
+        REQUIRE(elements_seen.find(element) == elements_seen.end());
+        elements_seen.insert(element);
+        element_counts[element]++;
+      }
+    }
+
+    for (const auto& iter : element_counts) {
+      REQUIRE(iter.second == expected_count);
+    }
+  }
+}
\ No newline at end of file
diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 7219803b71..f420c1cdeb 100644
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -283,6 +283,10 @@ set(XBT_SRC
   src/xbt/xbt_parse_units.cpp
   src/xbt/xbt_replay.cpp
   src/xbt/xbt_str.cpp
+  src/xbt/utils/iter/subsets.hpp
+  src/xbt/utils/iter/powerset.hpp
+  src/xbt/utils/iter/LazyKSubsets.hpp
+  src/xbt/utils/iter/LazyPowerset.hpp
   )
 
 if(HAVE_MMALLOC)
diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake
index ba1e45f9de..ce7d830116 100644
--- a/tools/cmake/Tests.cmake
+++ b/tools/cmake/Tests.cmake
@@ -126,6 +126,7 @@ set(UNIT_TESTS  src/xbt/unit-tests_main.cpp
                 src/xbt/dynar_test.cpp
                 src/xbt/random_test.cpp
                 src/xbt/xbt_str_test.cpp
+                src/xbt/utils/iter/subsets_tests.cpp
                 src/kernel/lmm/maxmin_test.cpp)
 
 set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp