Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Add full example for K-partial alternatives
authorMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 16 Mar 2023 09:56:36 +0000 (10:56 +0100)
committerMaxwell Pirtle <maxwellpirtle@gmail.com>
Thu, 16 Mar 2023 10:27:30 +0000 (11:27 +0100)
src/mc/explo/udpor/Configuration.cpp
src/mc/explo/udpor/Configuration_test.cpp
src/mc/explo/udpor/EventSet.cpp
src/mc/explo/udpor/EventSet.hpp

index c7e125d..7edc16e 100644 (file)
@@ -145,15 +145,15 @@ std::optional<Configuration> Configuration::compute_k_partial_alternative_to(con
   // NOTE: This is an expensive operation as we must traverse the entire unfolding
   // and compute `C.is_compatible_with(History)` for every event in the structure :/.
   // A later performance improvement would be to incorporate the work of Nguyen et al.
-  // into SimGrid. Since that is a rather complicated addition, we defer to the addition
-  // for a later time...
+  // into SimGrid which associated additonal data structures with each unfolding event.
+  // Since that is a rather complicated addition, we defer it to a later time...
   Comb comb(k);
 
   for (const auto* e : U) {
     for (unsigned i = 0; i < k; i++) {
       const UnfoldingEvent* e_i = D_hat[i];
       if (const auto e_local_config = History(e);
-          e_i->conflicts_with(e) and (not D.contains(e_local_config)) and is_compatible_with(e_local_config)) {
+          e_i->conflicts_with(e) and (not D.intersects(e_local_config)) and is_compatible_with(e_local_config)) {
         comb[i].push_back(e);
       }
     }
@@ -165,7 +165,8 @@ std::optional<Configuration> Configuration::compute_k_partial_alternative_to(con
   // NOTE: This is a VERY expensive operation: it enumerates all possible
   // ways to select an element from each spike. Unfortunately there's no
   // way around the enumeration, as computing a full alternative in general is
-  // NP-complete (although computing the k-partial alternative is polynomial in n)
+  // NP-complete (although computing the k-partial alternative is polynomial in
+  // the number of events)
   const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
     std::vector<const UnfoldingEvent*> events;
     for (const auto& event_in_spike : spikes) {
index 8506dd4..cff61e7 100644 (file)
@@ -614,7 +614,10 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
   //               e6       e10
   //
   // Theses tests walk through exactly the configurations and sets of `D` that
-  // UDPOR should encounter as it walks the unfolding.
+  // UDPOR COULD encounter as it walks through the unfolding. Note that
+  // if there are multiple alternatives to any given configuration, UDPOR can
+  // continue searching any one of them. The sequence assumes UDPOR first picks `e1`,
+  // then `e4`, and then `e7`
   Unfolding U;
 
   auto e0        = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
@@ -627,7 +630,7 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
   auto e2_handle = e2.get();
 
   auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
-  // auto e3_handle = e3.get();
+  auto e3_handle = e3.get();
 
   auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
   auto e4_handle = e4.get();
@@ -636,21 +639,45 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
   auto e5_handle = e5.get();
 
   auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+  auto e6_handle = e6.get();
 
   auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
   auto e7_handle = e7.get();
 
   auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+  auto e8_handle = e8.get();
 
-  auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<ConditionallyDependentAction>());
+  auto e9        = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<DependentAction>());
   auto e9_handle = e9.get();
 
   auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+  auto e10_handle = e10.get();
 
-  SECTION("Alternative computation step 1")
+  SECTION("Alternative computation call 1")
   {
-    const EventSet D;
+    // During the first call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /
+    //         /  /
+    //        e2 e3
+    //
+    // C := {e0, e1, e2} and `Explore(C, D, A)` picked `e3`
+    // (since en(C') where C' := {e0, e1, e2, e3} is empty
+    // [so UDPOR will simply return when C' is reached])
+    //
+    // Thus the computation is (since D is empty at first)
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3})
+    //
+    // where U is given above. There are no alternatives in
+    // this case since `e4` and `e7` conflict with `e1` (so
+    // they cannot be added to C to form a configuration)
     const Configuration C{e0_handle, e1_handle, e2_handle};
+    const EventSet D_plus_e{e3_handle};
 
     REQUIRE(U.empty());
     U.insert(std::move(e0));
@@ -660,14 +687,70 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
     U.insert(std::move(e4));
     U.insert(std::move(e7));
 
-    const auto alternative = C.compute_alternative_to(D, U);
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
     REQUIRE_FALSE(alternative.has_value());
   }
 
-  SECTION("Alternative computation step 2")
+  SECTION("Alternative computation call 2")
   {
-    const EventSet D{e1_handle};
+    // During the second call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /
+    //         /  /
+    //        e2 e3
+    //
+    // C := {e0, e1} and `Explore(C, D, A)` picked `e2`.
+    //
+    // Thus the computation is (since D is still empty)
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e1}, {e2})
+    //
+    // where U is given above. There are no alternatives in
+    // this case since `e4` and `e7` conflict with `e1` (so
+    // they cannot be added to C to form a configuration) and
+    // e3 is NOT in conflict with either e0 or e1
+    const Configuration C{e0_handle, e1_handle};
+    const EventSet D_plus_e{e2_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e7));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 3")
+  {
+    // During the thrid call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                 e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /
+    //         /  /
+    //        e2 e3
+    //
+    // C := {e0} and `Explore(C, D, A)` picked `e1`.
+    //
+    // Thus the computation is (since D is still empty)
+    //
+    // Alt(C, D + {e}) --> Alt({e0}, {e1})
+    //
+    // where U is given above. There are two alternatives in this case:
+    // {e0, e4} and {e0, e7}. Either one would be a valid choice for
+    // UDPOR, so we must check for the precense of either
     const Configuration C{e0_handle};
+    const EventSet D_plus_e{e1_handle};
 
     REQUIRE(U.empty());
     U.insert(std::move(e0));
@@ -677,7 +760,7 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
     U.insert(std::move(e4));
     U.insert(std::move(e7));
 
-    const auto alternative = C.compute_alternative_to(D, U);
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
     REQUIRE(alternative.has_value());
 
     // The first alternative that is found is the one that is chosen. Since
@@ -686,4 +769,395 @@ TEST_CASE("simgrid::mc::udpor:Configuration: Computing Full Alternatives in Read
     REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
              alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
   }
+
+  SECTION("Alternative computation call 4")
+  {
+    // During the fourth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //
+    //         /  /   e5  e8
+    //        e2 e3   /
+    //               e6
+    //
+    // C := {e0, e4, e5} and `Explore(C, D, A)` picked `e6`
+    // (since en(C') where C' := {e0, e4, e5, e6} is empty
+    // [so UDPOR will simply return when C' is reached])
+    //
+    // Thus the computation is (since D is {e1})
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6})
+    //
+    // where U is given above. There are no alternatives in this
+    // case, since:
+    //
+    // 1.`e2/e3` are eliminated since their histories contain `e1`
+    // 2. `e7/e8` are eliminated because they conflict with `e5`
+    const Configuration C{e0_handle, e4_handle, e5_handle};
+    const EventSet D_plus_e{e1_handle, e6_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 5")
+  {
+    // During the fifth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //
+    //         /  /   e5  e8
+    //        e2 e3   /
+    //               e6
+    //
+    // C := {e0, e4} and `Explore(C, D, A)` picked `e5`
+    // (since en(C') where C' := {e0, e4, e5, e6} is empty
+    // [so UDPOR will simply return when C' is reached])
+    //
+    // Thus the computation is (since D is {e1})
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5})
+    //
+    // where U is given above. There is one alternative in this case,
+    // viz. {e0, e4, e7, e8}.
+    //
+    // To continue the search, UDPOR computes J / C which in this
+    // case gives {e7, e8}. Since `e8` is not in en(C), UDPOR will
+    // choose `e7` next and add `e5` to `D`
+    const Configuration C{e0_handle, e4_handle};
+    const EventSet D_plus_e{e1_handle, e5_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE(alternative.has_value());
+    REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle}));
+  }
+
+  SECTION("Alternative computation call 6")
+  {
+    // During the sixth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                 e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /
+    //               e6
+    //
+    // C := {e0, e4, e7} and `Explore(C, D, A)` picked `e8`
+    // (since en(C') where C' := {e0, e4, e7, e8} is empty
+    // [so UDPOR will simply return when C' is reached])
+    //
+    // Thus the computation is (since D is {e1, e5} [see the last step])
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8})
+    //
+    // where U is given above. There are no alternatives in this case
+    // since all `e9` conflicts with `e4` and all other events of `U`
+    // are eliminated since their history intersects `D`
+    const Configuration C{e0_handle, e4_handle, e7_handle};
+    const EventSet D_plus_e{e1_handle, e5_handle, e8_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 7")
+  {
+    // During the seventh call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                 e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /
+    //               e6
+    //
+    // C := {e0, e4} and `Explore(C, D, A)` picked `e7`
+    //
+    // Thus the computation is (since D is {e1, e5} [see call 5])
+    //
+    // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7})
+    //
+    // where U is given above. There are no alternatives again in this case
+    // since all `e9` conflicts with `e4` and all other events of `U`
+    // are eliminated since their history intersects `D`
+    const Configuration C{e0_handle, e4_handle};
+    const EventSet D_plus_e{e1_handle, e5_handle, e7_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 8")
+  {
+    // During the eigth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                 e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /
+    //               e6
+    //
+    // C := {e0} and `Explore(C, D, A)` picked `e4`. At this
+    // point, UDPOR finished its recursive search of {e0, e4}
+    // after having finished {e0, e1} prior.
+    //
+    // Thus the computation is (since D = {e1})
+    //
+    // Alt(C, D + {e}) --> Alt({e0}, {e1, e4})
+    //
+    // where U is given above. There is one alternative in this
+    // case, viz {e0, e7, e9} since
+    // 1. e9 conflicts with e4 in D
+    // 2. e7 conflicts with e1 in D
+    // 3. the set {e7, e9} is conflict-free since `e7 < e9`
+    // 4. all other events are eliminated since their histories
+    // intersect D
+    //
+    // UDPOR will continue its recursive search following `e7`
+    // and add `e4` to D
+    const Configuration C{e0_handle};
+    const EventSet D_plus_e{e1_handle, e4_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE(alternative.has_value());
+    REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+  }
+
+  SECTION("Alternative computation call 9")
+  {
+    // During the ninth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /        /
+    //               e6       e10
+    //
+    // C := {e0, e7, e9} and `Explore(C, D, A)` picked `e10`.
+    // (since en(C') where C' := {e0, e7, e9, e10} is empty
+    // [so UDPOR will simply return when C' is reached]).
+    //
+    // Thus the computation is (since D = {e1, e4} [see the previous step])
+    //
+    // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10})
+    //
+    // where U is given above. There are no alternatives in this case
+    const Configuration C{e0_handle, e7_handle, e9_handle};
+    const EventSet D_plus_e{e1_handle, e4_handle, e10_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+    U.insert(std::move(e10));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 10")
+  {
+    // During the tenth call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /        /
+    //               e6       e10
+    //
+    // C := {e0, e7} and `Explore(C, D, A)` picked `e9`.
+    //
+    // Thus the computation is (since D = {e1, e4} [see call 8])
+    //
+    // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9})
+    //
+    // where U is given above. There are no alternatives in this case
+    const Configuration C{e0_handle, e7_handle};
+    const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+    U.insert(std::move(e10));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation call 11 (final call)")
+  {
+    // During the eleventh and final call to Alt(C, D + {e}),
+    // UDPOR believes `U` to be the following:
+    //
+    //                  e0
+    //              /  /   /
+    //            e1   e4   e7
+    //           /     /  //   /
+    //         /  /   e5  e8   e9
+    //        e2 e3   /        /
+    //               e6       e10
+    //
+    // C := {e0} and `Explore(C, D, A)` picked `e7`.
+    //
+    // Thus the computation is (since D = {e1, e4} [see call 8])
+    //
+    // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7})
+    //
+    // where U is given above. There are no alternatives in this case:
+    // everyone is eliminated!
+    const Configuration C{e0_handle, e7_handle};
+    const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
+
+    REQUIRE(U.empty());
+    U.insert(std::move(e0));
+    U.insert(std::move(e1));
+    U.insert(std::move(e2));
+    U.insert(std::move(e3));
+    U.insert(std::move(e4));
+    U.insert(std::move(e6));
+    U.insert(std::move(e7));
+    U.insert(std::move(e8));
+    U.insert(std::move(e9));
+    U.insert(std::move(e10));
+
+    const auto alternative = C.compute_alternative_to(D_plus_e, U);
+    REQUIRE_FALSE(alternative.has_value());
+  }
+
+  SECTION("Alternative computation next")
+  {
+    SECTION("Followed {e0, e7} first")
+    {
+      const EventSet D{e1_handle, e7_handle};
+      const Configuration C{e0_handle};
+
+      REQUIRE(U.empty());
+      U.insert(std::move(e0));
+      U.insert(std::move(e1));
+      U.insert(std::move(e2));
+      U.insert(std::move(e3));
+      U.insert(std::move(e4));
+      U.insert(std::move(e5));
+      U.insert(std::move(e7));
+      U.insert(std::move(e8));
+      U.insert(std::move(e9));
+      U.insert(std::move(e10));
+
+      const auto alternative = C.compute_alternative_to(D, U);
+      REQUIRE(alternative.has_value());
+
+      // In this case, only {e0, e4} is a valid alternative
+      REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle}));
+    }
+
+    SECTION("Followed {e0, e4} first")
+    {
+      const EventSet D{e1_handle, e4_handle};
+      const Configuration C{e0_handle};
+
+      REQUIRE(U.empty());
+      U.insert(std::move(e0));
+      U.insert(std::move(e1));
+      U.insert(std::move(e2));
+      U.insert(std::move(e3));
+      U.insert(std::move(e4));
+      U.insert(std::move(e5));
+      U.insert(std::move(e6));
+      U.insert(std::move(e7));
+      U.insert(std::move(e8));
+      U.insert(std::move(e9));
+
+      const auto alternative = C.compute_alternative_to(D, U);
+      REQUIRE(alternative.has_value());
+
+      // In this case, only {e0, e7} is a valid alternative
+      REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
+    }
+  }
 }
\ No newline at end of file
index ea42f8b..09cb66b 100644 (file)
@@ -137,6 +137,11 @@ bool EventSet::contains(const History& history) const
   return std::all_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
 }
 
+bool EventSet::intersects(const History& history) const
+{
+  return std::any_of(history.begin(), history.end(), [=](const UnfoldingEvent* e) { return this->contains(e); });
+}
+
 bool EventSet::is_maximal() const
 {
   // A set of events is maximal if no event from
index 37da51a..54c00c8 100644 (file)
@@ -54,6 +54,7 @@ public:
   bool empty() const;
   bool contains(const UnfoldingEvent*) const;
   bool contains(const History&) const;
+  bool intersects(const History&) const;
   bool is_subset_of(const EventSet&) const;
 
   bool operator==(const EventSet& other) const { return this->events_ == other.events_; }