Implement adding events to configurations

When adding an event to a configuration, we
assert that the configuration actually contains
all of the dependencies of that event within it;
otherwise, we would violate the property that a
configuration contains all of its dependencies.

Note that we do not assert whether or not the
configuration is actually conflict-free: we leave
that to the correctness of UDPOR and other tests which
will assert UDPOR is doing the right thing. But having
this assertion will certainly help catch bugs with the
UDPOR implementation more quickly (termination would
happen at the moment that the algorithm encounters
a spot where it chose an event incorrectly).

diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp
index 084854d..d6e42d3 100644 (file)
--- a/src/mc/explo/udpor/Configuration.cpp
+++ b/src/mc/explo/udpor/Configuration.cpp
@@ -4,6 +4,10 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/History.hpp"
+
+#include <algorithm>
+#include <stdexcept>
 
 namespace simgrid::mc::udpor {
 
@@ -12,7 +16,11 @@ void Configuration::add_event(UnfoldingEvent* e)
   this->events_.insert(e);
   this->newest_event = e;
 
-  // TODO: Re-compute the maxmimal events
+  History history(e);
+  if (!this->events_.contains(history)) {
+    throw std::invalid_argument("The newly added event has dependencies "
+                                "which are missing from this configuration");
+  }
 }
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index 6c80b3d..27595e5 100644 (file)
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -18,14 +18,39 @@ public:
   Configuration& operator=(Configuration const&) = default;
   Configuration(Configuration&&)                 = default;
 
+  Configuration(EventSet events) : events_(events) {}
+  Configuration(EventSet&& events) : events_(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); }
   const EventSet& get_events() const { return this->events_; }
-  const EventSet& get_maximal_events() const { return this->max_events_; }
   UnfoldingEvent* get_latest_event() const { return this->newest_event; }
 
+  /**
+   * @brief Insert a new event into the configuration
+   *
+   * When the newly added event is inserted into the configuration,
+   * an assertion is made to ensure that the configuration remains
+   * valid, i.e. that the newly added event's dependencies are contained
+   * within the configuration.
+   *
+   * @throws an invalid argument exception is raised should the event
+   * be missing one of its dependencies
+   *
+   * @note: UDPOR technically enforces the invariant that all newly-added events
+   * will ensure that the configuration is valid. We perform extra checks to ensure
+   * that UDPOR is implemented as expected. There is a performance penalty that
+   * should be noted: checking for maximality requires ensuring that all events in the
+   * configuration have their dependencies containes within the configuration, which
+   * essentially means performing a BFS/DFS over the configuration using a History object.
+   * However, since the slowest part of UDPOR involves enumerating all
+   * subsets of maximal events and computing k-partial alternatives (the
+   * latter definitively an NP-hard problem when optimal), Amdahl's law suggests
+   * we shouldn't focus so much on this (let alone the additional benefit of the
+   * assertions)
+   */
   void add_event(UnfoldingEvent*);
 
 private:
@@ -39,29 +64,8 @@ private:
    *
    * @invariant For each event `e` in `events_`, the set of
    * dependencies of `e` is also contained in `events_`
-   *
-   * TODO: UDPOR enforces this invariant, but perhaps we should
-   * too?
    */
   EventSet events_;
-
-  /**
-   * The <-maxmimal events of the configuration. These are
-   * dynamically adjusted as events are added to the configuration
-   *
-   * @invariant Each event that is part of this set is
-   *
-   * 1. a <-maxmimal event of the configuration, in the sense that
-   * there is no event in the configuration that is "greater" than it.
-   * In UDPOR terminology, each event does not "cause" another event
-   *
-   * 2. contained in the set of events `events_` which comprise
-   * the configuration
-   */
-  EventSet max_events_;
-
-private:
-  void recompute_maxmimal_events(UnfoldingEvent* new_event);
 };
 
 } // namespace simgrid::mc::udpor

diff --git a/src/mc/explo/udpor/EventSet.cpp b/src/mc/explo/udpor/EventSet.cpp
index aee945f..6f486b7 100644 (file)
--- a/src/mc/explo/udpor/EventSet.cpp
+++ b/src/mc/explo/udpor/EventSet.cpp
@@ -120,6 +120,11 @@ bool EventSet::is_valid_configuration() const
   /// The proof is based on the definition of a configuration
   /// which requires that all
   const History history(*this);
+  return this->contains(history);
+}
+
+bool EventSet::contains(const History& history) const
+{
   return std::all_of(history.begin(), history.end(), [=](UnfoldingEvent* e) { return this->contains(e); });
 }
 

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

diff --git a/src/mc/explo/udpor/History_test.cpp b/src/mc/explo/udpor/History_test.cpp
index 961aaaa..0cbe878 100644 (file)
--- a/src/mc/explo/udpor/History_test.cpp
+++ b/src/mc/explo/udpor/History_test.cpp
@@ -209,9 +209,4 @@ TEST_CASE("simgrid::mc::udpor::History: History generation")
       REQUIRE(history.contains(&e7));
     }
   }
-
-  SECTION("History with masking configuration")
-  {
-    Configuration configuration;
-  }
 }