Add conflict-free invariant check to Configuration

When adding events to a configuration, we want to
ensure that the configuration remains both a)
causally closed and b) conflict-free. The latter
required that the tests be modified as they effectively
assumed that the transitions associated with each
event were independent of one another. Since the
`Transition` base class is dependent by default, this
was at odds with the assumptions

diff --git a/src/mc/explo/udpor/Configuration.cpp b/src/mc/explo/udpor/Configuration.cpp
index a1b7924..8e2cb85 100644 (file)
--- a/src/mc/explo/udpor/Configuration.cpp
+++ b/src/mc/explo/udpor/Configuration.cpp
@@ -36,12 +36,18 @@ void Configuration::add_event(const UnfoldingEvent* e)
     return;
   }
 
+  // Preserves the property that the configuration is conflict-free
+  if (e->conflicts_with(*this)) {
+    throw std::invalid_argument("The newly added event conflicts with the events already "
+                                "contained in the configuration. Adding this event violates "
+                                "the property that a configuration is conflict-free");
+  }
+
   this->events_.insert(e);
   this->newest_event = e;
 
-  // Preserves the property that the configuration is valid
-  History history(e);
-  if (!this->events_.contains(history)) {
+  // Preserves the property that the configuration is causally closed
+  if (auto history = History(e); !this->events_.contains(history)) {
     throw std::invalid_argument("The newly added event has dependencies "
                                 "which are missing from this configuration");
   }

diff --git a/src/mc/explo/udpor/Configuration.hpp b/src/mc/explo/udpor/Configuration.hpp
index 3b344dd..a27b9a6 100644 (file)
--- a/src/mc/explo/udpor/Configuration.hpp
+++ b/src/mc/explo/udpor/Configuration.hpp
@@ -23,6 +23,8 @@ public:
 
   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(); }
 
   bool contains(const UnfoldingEvent* e) const { return this->events_.contains(e); }
   const EventSet& get_events() const { return this->events_; }

diff --git a/src/mc/explo/udpor/Configuration_test.cpp b/src/mc/explo/udpor/Configuration_test.cpp
index af975fc..48eeb4e 100644 (file)
--- a/src/mc/explo/udpor/Configuration_test.cpp
+++ b/src/mc/explo/udpor/Configuration_test.cpp
@@ -9,6 +9,7 @@
 #include "src/mc/explo/udpor/History.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
+#include "src/mc/explo/udpor/udpor_tests_private.hpp"
 
 #include <unordered_map>
 
@@ -24,11 +25,11 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
   //          e3
   //         /  /
   //        e4   e5
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3};
-  UnfoldingEvent e5{&e3};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>());
 
   SECTION("Creating a configuration without events")
   {
@@ -37,7 +38,7 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
     REQUIRE(C.get_latest_event() == nullptr);
   }
 
-  SECTION("Creating a configuration with events")
+  SECTION("Creating a configuration with events (test violation of being causally closed)")
   {
     // 5 choose 0 = 1 test
     REQUIRE_NOTHROW(Configuration({&e1}));
@@ -93,10 +94,10 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events")
   //           /
   //         /  /
   //        e3   e4
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e2};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
 
   REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument);
   REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument);
@@ -136,10 +137,10 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order")
   //          e3
   //         /
   //        e4
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
 
   SECTION("Topological ordering for entire set")
   {
@@ -194,12 +195,12 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Compli
   //        e4   e6
   //        /
   //       e5
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3};
-  UnfoldingEvent e5{&e4};
-  UnfoldingEvent e6{&e3};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>());
 
   SECTION("Topological ordering for subsets")
   {
@@ -303,18 +304,18 @@ TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Compli
   //        /   /     /
   //         /  /   /
   //         [   e12    ]
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e8{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3};
-  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};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e8(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e6(EventSet({&e4}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e7(EventSet({&e2, &e8}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e9(EventSet({&e6, &e7}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e10(EventSet({&e7}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e12(EventSet({&e5, &e9, &e10}), std::make_shared<IndependentAction>());
   Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
 
   SECTION("Test every combination of the maximal configuration (forward graph)")
@@ -405,14 +406,14 @@ TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Basic Testing of Maxima
   //           e3    e6
   //           /     / /
   //          e4    e7 e8
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e2};
-  UnfoldingEvent e4{&e3};
-  UnfoldingEvent e5{&e1};
-  UnfoldingEvent e6{&e5};
-  UnfoldingEvent e7{&e6};
-  UnfoldingEvent e8{&e6};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e8(EventSet({&e6}), std::make_shared<IndependentAction>());
 
   SECTION("Iteration over an empty configuration yields only the empty set")
   {
@@ -538,24 +539,24 @@ TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal
   //               |   e11 e12 e13 e14   e15
   //               |   /      / / /   /  /
   //               +-> e16     e17     e18
-  UnfoldingEvent e1;
-  UnfoldingEvent e2{&e1};
-  UnfoldingEvent e3{&e1};
-  UnfoldingEvent e4{&e2};
-  UnfoldingEvent e5{&e2};
-  UnfoldingEvent e6{&e3};
-  UnfoldingEvent e7{&e3};
-  UnfoldingEvent e8{&e4};
-  UnfoldingEvent e9{&e4, &e5, &e6};
-  UnfoldingEvent e10{&e6, &e7};
-  UnfoldingEvent e11{&e8};
-  UnfoldingEvent e12{&e8};
-  UnfoldingEvent e13{&e9};
-  UnfoldingEvent e14{&e9};
-  UnfoldingEvent e15{&e10};
-  UnfoldingEvent e16{&e5, &e11};
-  UnfoldingEvent e17{&e12, &e13, &e14};
-  UnfoldingEvent e18{&e14, &e15};
+  UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+  UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e5(EventSet({&e2}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e7(EventSet({&e3}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e8(EventSet({&e4}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e9(EventSet({&e4, &e5, &e6}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e10(EventSet({&e6, &e7}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e12(EventSet({&e8}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e13(EventSet({&e9}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e14(EventSet({&e9}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e15(EventSet({&e10}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e16(EventSet({&e5, &e11}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e17(EventSet({&e12, &e13, &e14}), std::make_shared<IndependentAction>());
+  UnfoldingEvent e18(EventSet({&e14, &e15}), std::make_shared<IndependentAction>());
   Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12, &e13, &e14, &e15, &e16, &e17, &e18};
 
   SECTION("Every subset iterated over is maximal")

diff --git a/src/mc/explo/udpor/EventSet_test.cpp b/src/mc/explo/udpor/EventSet_test.cpp
index de0822a..62109a4 100644 (file)
--- a/src/mc/explo/udpor/EventSet_test.cpp
+++ b/src/mc/explo/udpor/EventSet_test.cpp
@@ -6,9 +6,9 @@
 #include "src/3rd-party/catch.hpp"
 #include "src/mc/explo/udpor/EventSet.hpp"
 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
+#include "src/mc/explo/udpor/udpor_tests_private.hpp"
 #include "src/mc/transition/Transition.hpp"
 
-using namespace simgrid::mc;
 using namespace simgrid::mc::udpor;
 
 TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets")
@@ -761,27 +761,6 @@ TEST_CASE("simgrid::mc::udpor::EventSet: Moving into a collection")
 
 TEST_CASE("simgrid::mc::udpor::EventSet: Checking conflicts")
 {
-  struct IndependentAction : public Transition {
-    // Independent with everyone else
-    bool depends(const Transition* other) const override { return false; }
-  };
-
-  struct DependentAction : public Transition {
-    // Dependent with everyone else (except IndependentAction)
-    bool depends(const Transition* other) const override
-    {
-      return dynamic_cast<const IndependentAction*>(other) == nullptr;
-    }
-  };
-
-  struct ConditionallyDependentAction : public Transition {
-    // Dependent only with DependentAction (i.e. not itself)
-    bool depends(const Transition* other) const override
-    {
-      return dynamic_cast<const DependentAction*>(other) != nullptr;
-    }
-  };
-
   // The following tests concern the given event structure:
   //                e1
   //              /    /

diff --git a/src/mc/explo/udpor/UnfoldingEvent.cpp b/src/mc/explo/udpor/UnfoldingEvent.cpp
index bd49e86..83e1d7d 100644 (file)
--- a/src/mc/explo/udpor/UnfoldingEvent.cpp
+++ b/src/mc/explo/udpor/UnfoldingEvent.cpp
@@ -74,6 +74,18 @@ bool UnfoldingEvent::conflicts_with(const UnfoldingEvent* other) const
   return false;
 }
 
+bool UnfoldingEvent::conflicts_with(const Configuration& config) const
+{
+  // A configuration is itself already conflict-free. Thus, it is
+  // simply a matter of testing whether or not the transition associated
+  // with the event is dependent with any already in `config` that are
+  // OUTSIDE this event's history (in an unfolding, events only conflict
+  // if they are not related)
+  const EventSet potential_conflicts = config.get_events().subtracting(get_history());
+  return std::any_of(potential_conflicts.cbegin(), potential_conflicts.cend(),
+                     [&](const UnfoldingEvent* e) { return this->has_conflicting_transition_with(e); });
+}
+
 bool UnfoldingEvent::has_conflicting_transition_with(const UnfoldingEvent* other) const
 {
   return associated_transition->depends(other->associated_transition.get());

diff --git a/src/mc/explo/udpor/udpor_forward.hpp b/src/mc/explo/udpor/udpor_forward.hpp
index 865df16..1cbdb2e 100644 (file)
--- a/src/mc/explo/udpor/udpor_forward.hpp
+++ b/src/mc/explo/udpor/udpor_forward.hpp
@@ -3,7 +3,7 @@
 /* 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. */
 
-/** @file mc_forward.hpp
+/** @file udpor_forward.hpp
  *
  *  Forward definitions for MC types specific to UDPOR
  */

diff --git a/src/mc/explo/udpor/udpor_tests_private.hpp b/src/mc/explo/udpor/udpor_tests_private.hpp
new file mode 100644 (file)
index 0000000..6e1a233
--- /dev/null
+++ b/src/mc/explo/udpor/udpor_tests_private.hpp
@@ -0,0 +1,40 @@
+/* Copyright (c) 2007-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. */
+
+/** @file udpor_tests_private.hpp
+ *
+ * A private header file for tests involving events in
+ * configurations
+ */
+
+#ifndef SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
+#define SIMGRID_MC_UDPOR_TEST_PRIVATE_HPP
+
+namespace simgrid::mc::udpor {
+
+struct IndependentAction : public Transition {
+  // Independent with everyone else
+  bool depends(const Transition* other) const override { return false; }
+};
+
+struct DependentAction : public Transition {
+  // Dependent with everyone else (except IndependentAction)
+  bool depends(const Transition* other) const override
+  {
+    return dynamic_cast<const IndependentAction*>(other) == nullptr;
+  }
+};
+
+struct ConditionallyDependentAction : public Transition {
+  // Dependent only with DependentAction (i.e. not itself)
+  bool depends(const Transition* other) const override
+  {
+    return dynamic_cast<const DependentAction*>(other) != nullptr;
+  }
+};
+
+} // namespace simgrid::mc::udpor
+
+#endif