Add method to check if an EventSet is a config

A method was added that determines whether or not
some set of events (i.e. an `EventSet`) are actually
a valid configuration or not. The question of choosing
valid configurations is up to UDPOR, so while enforcing
that each and every event added to a configuration
be checked to ensure that the configuration remains
as such, it is not strictly necessary. However, it
will help us identify bugs with configurations if
and when they arise.

The key idea behind checking whether a set of events
forms a configuration is to again leverage the power
of History. If while searching through the history
of a set of events you stumble upon an event that is
not part of the original group, then you know that
said group cannot be a configuration since at least
one of the member's dependencies are not part of the
group.

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index 1ec91db..681a272 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -5,6 +5,7 @@
 
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
 
 #include <iterator>
 
@@ -107,4 +108,17 @@ bool EventSet::is_subset_of(const EventSet& other) const
   return subtracting(other).empty();
 }
 
+bool EventSet::is_valid_configuration() const
+{
+  /// @invariant: A collection of events `E` is a configuration
+  /// if and only if following while following the history of
+  /// each event `e` of `E`you remain in `E`. In other words, you
+  /// only see events from set `E`
+  ///
+  /// The proof is based on the definition of a configuration
+  /// which requires that all
+  const History history(*this);
+  return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
+}
+
 } // namespace simgrid::mc::udpor
\ No newline at end of file

diff --git a/src/mc/explo/udpor/EventSet.hpp b/src/mc/explo/udpor/EventSet.hpp
index f59593e..9488c1b 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -50,6 +50,7 @@ public:
   bool empty() const;
   bool contains(UnfoldingEvent*) const;
   bool is_subset_of(const EventSet&) const;
+  bool is_valid_configuration() const;
 
   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }
   bool operator!=(const EventSet& other) const { return this->events_ != other.events_; }

diff --git a/src/mc/explo/udpor/History.cpp b/src/mc/explo/udpor/History.cpp
index 76b9eff..6af39ef 100644 (file)
--- a/src/mc/explo/udpor/History.cpp
+++ b/src/mc/explo/udpor/History.cpp
@@ -11,6 +11,11 @@
 
 namespace simgrid::mc::udpor {
 
+History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
+    : frontier(initial_events), configuration(config)
+{
+}
+
 History::Iterator& History::Iterator::operator++()
 {
   if (not frontier.empty()) {
@@ -18,8 +23,6 @@ History::Iterator& History::Iterator::operator++()
     UnfoldingEvent* e = *frontier.begin();
     frontier.remove(e);
 
-    // If we've seen this event before, skip it
-
     // If there is a configuration and if the
     // event is in it, skip it: the event and
     // all of its immediate causes do not need to
@@ -34,8 +37,8 @@ History::Iterator& History::Iterator::operator++()
 
     // Perform the expansion with all viable expansions
     EventSet candidates = e->get_immediate_causes();
-    candidates.subtract(current_history);
 
+    candidates.subtract(current_history);
     frontier.form_union(std::move(candidates));
   }
   return *this;
@@ -59,16 +62,14 @@ bool History::contains(UnfoldingEvent* e) const
 
 EventSet History::get_event_diff_with(const Configuration& config) const
 {
-  // auto wrapped_config = std::optional<std::reference_wrapper<Configuration>>(config);
-  // auto first          = Iterator(events_, wrapped_config);
-  // const auto last     = this->end();
+  auto wrapped_config = std::optional<std::reference_wrapper<const Configuration>>{config};
+  auto first          = Iterator(events_, std::move(wrapped_config));
+  const auto last     = this->end();
 
-  // for (; first != last; ++first)
-  //   ;
+  for (; first != last; ++first)
+    ;
 
-  // return first.current_history;
-  // TODO: Implement this
-  return EventSet();
+  return first.current_history;
 }
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp
index d4b9753..4815496 100644 (file)
--- a/src/mc/explo/udpor/History.hpp
+++ b/src/mc/explo/udpor/History.hpp
@@ -92,19 +92,7 @@ private:
    * @brief An iterator which traverses the history of a set of events
    */
   struct Iterator {
-  private:
-    EventSet frontier;
-    EventSet current_history = EventSet();
-    std::optional<std::reference_wrapper<Configuration>> configuration;
-
-    friend History;
-
   public:
-    Iterator(const EventSet& initial_events, std::optional<std::reference_wrapper<Configuration>> config = std::nullopt)
-        : frontier(initial_events), configuration(config)
-    {
-    }
-
     Iterator& operator++();
     auto operator->() { return frontier.begin().operator->(); }
     auto operator*() const { return *frontier.begin(); }
@@ -115,11 +103,20 @@ private:
     bool operator==(const Iterator& other) { return this->frontier == other.frontier; }
     bool operator!=(const Iterator& other) { return not(this->operator==(other)); }
 
-    using iterator_category = std::forward_iterator_tag;
-    using difference_type   = int; // # of steps between
-    using value_type        = UnfoldingEvent*;
-    using pointer           = value_type*;
-    using reference         = value_type&;
+    using iterator_category      = std::forward_iterator_tag;
+    using difference_type        = int; // # of steps between
+    using value_type             = UnfoldingEvent*;
+    using pointer                = value_type*;
+    using reference              = value_type&;
+    using optional_configuration = std::optional<std::reference_wrapper<const Configuration>>;
+
+    Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
+
+  private:
+    EventSet frontier;
+    EventSet current_history = EventSet();
+    optional_configuration configuration;
+    friend History;
   };
 };
 

diff --git a/src/mc/explo/udpor/History_test.cpp b/src/mc/explo/udpor/History_test.cpp
index a1fbd1a..961aaaa 100644 (file)
--- a/src/mc/explo/udpor/History_test.cpp
+++ b/src/mc/explo/udpor/History_test.cpp
@@ -170,7 +170,7 @@ TEST_CASE("simgrid::mc::udpor::History: History generation")
       REQUIRE_FALSE(history_e3e5.contains(&e7));
     }
 
-    SECTION("Nodes with the different ancestors")
+    SECTION("Nodes with different ancestors")
     {
       History history_e4e7(EventSet({&e4, &e7}));
       REQUIRE(history_e4e7.get_all_events() == EventSet({&e1, &e2, &e4, &e6, &e7}));
@@ -196,17 +196,22 @@ TEST_CASE("simgrid::mc::udpor::History: History generation")
       REQUIRE_FALSE(history_e2356.contains(&e7));
     }
 
-    SECTION("History of the entire graph is the entire graph")
+    SECTION("History of the entire graph yields the entire graph")
     {
-      History history_e2356(EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
-      REQUIRE(history_e2356.get_all_events() == EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
-      REQUIRE(history_e2356.contains(&e1));
-      REQUIRE(history_e2356.contains(&e2));
-      REQUIRE(history_e2356.contains(&e3));
-      REQUIRE(history_e2356.contains(&e4));
-      REQUIRE(history_e2356.contains(&e5));
-      REQUIRE(history_e2356.contains(&e6));
-      REQUIRE(history_e2356.contains(&e7));
+      History history(EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
+      REQUIRE(history.get_all_events() == EventSet({&e1, &e2, &e3, &e4, &e5, &e6, &e7}));
+      REQUIRE(history.contains(&e1));
+      REQUIRE(history.contains(&e2));
+      REQUIRE(history.contains(&e3));
+      REQUIRE(history.contains(&e4));
+      REQUIRE(history.contains(&e5));
+      REQUIRE(history.contains(&e6));
+      REQUIRE(history.contains(&e7));
     }
   }
+
+  SECTION("History with masking configuration")
+  {
+    Configuration configuration;
+  }
 }