Add extensive tests for checking valid configurations

An example event structure was given and all
possible subsets of its events were tested for
completeness. Each subset was tested for whether
it was a maximal subset of events (i.e. one for
which no element causes any of the others) and
for whether the set of events qualified for being
a configuration.

An additional observation was made concerning the determination of
whether or not a set of events is maximal. To compute
the maximal events of a given set of events, it suffices
to search the entire history of the events and eliminate
events from the original set as they appear. Note that only
events in the set itself can ever be maximal, as all other
events discovered in the search must have come from one
of these event's dependencies, or one of their dependencies'
dependencies, and so on.

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index 681a272..aee945f 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -11,6 +11,8 @@
 
 namespace simgrid::mc::udpor {
 
+EventSet::EventSet(Configuration&& config) : EventSet(std::move(config.get_events())) {}
+
 void EventSet::remove(UnfoldingEvent* e)
 {
   this->events_.erase(e);
@@ -121,4 +123,10 @@ bool EventSet::is_valid_configuration() const
   return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
 }
 
+bool EventSet::is_maximal_event_set() const
+{
+  const History history(*this);
+  return *this == history.get_all_maximal_events();
+}
+
 } // 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 9488c1b..8673066 100644 (file)
--- a/src/mc/explo/udpor/EventSet.hpp
+++ b/src/mc/explo/udpor/EventSet.hpp
@@ -24,6 +24,7 @@ public:
   EventSet& operator=(const EventSet&) = default;
   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)) {}
 
@@ -50,10 +51,23 @@ 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_; }
+
+public:
+  /**
+   * @brief Whether or not this set of events could
+   * represent a configuration
+   */
+  bool is_valid_configuration() const;
+
+  /**
+   * @brief Whether or not this set of events is
+   * a *maximal event set*, i.e. whether each element
+   * of the set causes none of the others
+   */
+  bool is_maximal_event_set() const;
 };
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp
index 72f5614..77a555d 100644 (file)
--- a/src/mc/explo/udpor/EventSet_test.cpp
+++ b/src/mc/explo/udpor/EventSet_test.cpp
@@ -502,4 +502,214 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Subset Tests")
       REQUIRE(F.is_subset_of(F));
     }
   }
+}
+
+TEST_CASE("simgrid::mc::udpor::EventSet: Testing Configurations")
+{
+  // The following tests concern the given event structure:
+  //                e1
+  //              /    /
+  //            e2      e5
+  //           /  /      /
+  //          e3  e4     e6
+  // The tests enumerate all possible subsets of the events
+  // 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 e6{&e5};
+
+  SECTION("Valid Configurations")
+  {
+    SECTION("The empty set is valid")
+    {
+      REQUIRE(EventSet().is_valid_configuration());
+    }
+
+    SECTION("The set with only the root event is valid")
+    {
+      REQUIRE(EventSet({&e1}).is_valid_configuration());
+    }
+
+    SECTION("All sets of maximal events are valid configurations")
+    {
+      REQUIRE(EventSet({&e1}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e5}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration());
+      REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+    }
+  }
+
+  SECTION("Configuration checks")
+  {
+    // 6 choose 0 = 1 test
+    REQUIRE(EventSet().is_valid_configuration());
+
+    // 6 choose 1 = 6 tests
+    REQUIRE(EventSet({&e1}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e4}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e6}).is_valid_configuration());
+
+    // 6 choose 2 = 15 tests
+    REQUIRE(EventSet({&e1, &e2}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e4}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e4}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e4}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e4, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e5, &e6}).is_valid_configuration());
+
+    // 6 choose 3 = 20 tests
+    REQUIRE(EventSet({&e1, &e2, &e3}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e4}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e4, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_valid_configuration());
+
+    // 6 choose 4 = 15 tests
+    REQUIRE(EventSet({&e1, &e2, &e3, &e4}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e3, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_valid_configuration());
+
+    // 6 choose 5 = 6 tests
+    REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_valid_configuration());
+    REQUIRE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_valid_configuration());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+
+    // 6 choose 6 = 1 test
+    REQUIRE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_valid_configuration());
+  }
+
+  SECTION("Maximal event sets")
+  {
+    // 6 choose 0 = 1 test
+    REQUIRE(EventSet().is_maximal_event_set());
+
+    // 6 choose 1 = 6 tests
+    REQUIRE(EventSet({&e1}).is_maximal_event_set());
+    REQUIRE(EventSet({&e2}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3}).is_maximal_event_set());
+    REQUIRE(EventSet({&e4}).is_maximal_event_set());
+    REQUIRE(EventSet({&e5}).is_maximal_event_set());
+    REQUIRE(EventSet({&e6}).is_maximal_event_set());
+
+    // 6 choose 2 = 15 tests
+    REQUIRE_FALSE(EventSet({&e1, &e2}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e4}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e4}).is_maximal_event_set());
+    REQUIRE(EventSet({&e2, &e5}).is_maximal_event_set());
+    REQUIRE(EventSet({&e2, &e6}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3, &e4}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3, &e5}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3, &e6}).is_maximal_event_set());
+    REQUIRE(EventSet({&e4, &e5}).is_maximal_event_set());
+    REQUIRE(EventSet({&e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e5, &e6}).is_maximal_event_set());
+
+    // 6 choose 3 = 20 tests
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e4}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e5, &e6}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3, &e4, &e5}).is_maximal_event_set());
+    REQUIRE(EventSet({&e3, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e3, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e4, &e5, &e6}).is_maximal_event_set());
+
+    // 6 choose 4 = 15 tests
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e4, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e4, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e3, &e4, &e5, &e6}).is_maximal_event_set());
+
+    // 6 choose 5 = 6 tests
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e4, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e1, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+    REQUIRE_FALSE(EventSet({&e2, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+
+    // 6 choose 6 = 1 test
+    REQUIRE_FALSE(EventSet({&e1, &e2, &e3, &e4, &e5, &e6}).is_maximal_event_set());
+  }
 }
\ No newline at end of file

diff --git a/src/mc/explo/udpor/History.cpp b/src/mc/explo/udpor/History.cpp
index 6af39ef..544980a 100644 (file)
--- a/src/mc/explo/udpor/History.cpp
+++ b/src/mc/explo/udpor/History.cpp
@@ -12,8 +12,12 @@
 namespace simgrid::mc::udpor {
 
 History::Iterator::Iterator(const EventSet& initial_events, optional_configuration config)
-    : frontier(initial_events), configuration(config)
+    : frontier(initial_events), maximal_events(initial_events), configuration(config)
 {
+  // NOTE: Only events in the initial set of events can ever hope to have
+  // a chance at being a maximal event, since all other events in
+  // the search are generate by looking at dependencies of these events
+  // and all subsequent events that are added by the iterator
 }
 
 History::Iterator& History::Iterator::operator++()
@@ -38,6 +42,8 @@ History::Iterator& History::Iterator::operator++()
     // Perform the expansion with all viable expansions
     EventSet candidates = e->get_immediate_causes();
 
+    maximal_events.subtract(candidates);
+
     candidates.subtract(current_history);
     frontier.form_union(std::move(candidates));
   }
@@ -55,6 +61,17 @@ EventSet History::get_all_events() const
   return first.current_history;
 }
 
+EventSet History::get_all_maximal_events() const
+{
+  auto first      = this->begin();
+  const auto last = this->end();
+
+  for (; first != last; ++first)
+    ;
+
+  return first.maximal_events;
+}
+
 bool History::contains(UnfoldingEvent* e) const
 {
   return std::any_of(this->begin(), this->end(), [=](UnfoldingEvent* e_hist) { return e == e_hist; });

diff --git a/src/mc/explo/udpor/History.hpp b/src/mc/explo/udpor/History.hpp
index 4815496..e667424 100644 (file)
--- a/src/mc/explo/udpor/History.hpp
+++ b/src/mc/explo/udpor/History.hpp
@@ -85,6 +85,14 @@ public:
    * dependency graph for all events in this history
    */
   EventSet get_all_events() const;
+
+  /**
+   * @brief Computes all events in the history described by this instance
+   * which are maximal (intuitively, those events which cause no others
+   * or are the "most recent")
+   */
+  EventSet get_all_maximal_events() const;
+
   EventSet get_event_diff_with(const Configuration& config) const;
 
 private:
@@ -113,8 +121,15 @@ private:
     Iterator(const EventSet& initial_events, optional_configuration config = std::nullopt);
 
   private:
+    /// @brief Points in the graph from where to continue the search
     EventSet frontier;
+
+    /// @brief What the iterator currently believes to be the
+    /// entire history of the events in the graph it traverses
     EventSet current_history = EventSet();
+
+    /// @brief What the iterator currently believes
+    EventSet maximal_events;
     optional_configuration configuration;
     friend History;
   };

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index 7294a64..ee6de7c 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -27,7 +27,7 @@ bool UnfoldingEvent::operator==(const UnfoldingEvent& other) const
 
   // All unfolding event objects are created in reference to
   // an Unfolding object which owns them. Hence, the references
-  // they contain to other events in the unvolding can
+  // they contain to other events in the unfolding can
   // be used as intrinsic identities (i.e. we don't need to
   // recursively check if each of our causes has a `==` in
   // the other event's causes)