src/mc/explo/udpor/Configuration_test.cpp

   1 /* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved.               */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/3rd-party/catch.hpp"
   7 #include "src/mc/explo/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/EventSet.hpp"
   9 #include "src/mc/explo/udpor/History.hpp"
  10 #include "src/mc/explo/udpor/Unfolding.hpp"
  11 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
  12 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
  13 #include "src/mc/explo/udpor/udpor_tests_private.hpp"
  14
  15 #include <unordered_map>
  16
  17 using namespace simgrid::mc;
  18 using namespace simgrid::mc::udpor;
  19
  20 TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
  21 {
  22   // The following tests concern the given event structure:
  23   //                e1
  24   //              /
  25   //            e2
  26   //           /
  27   //          e3
  28   //         /  /
  29   //        e4   e5
  30   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
  31   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
  32   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
  33   UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
  34   UnfoldingEvent e5(EventSet({&e3}), std::make_shared<IndependentAction>(4));
  35
  36   SECTION("Creating a configuration without events")
  37   {
  38     Configuration C;
  39     REQUIRE(C.get_events().empty());
  40     REQUIRE(C.get_latest_event() == nullptr);
  41   }
  42
  43   SECTION("Creating a configuration with events (test violation of being causally closed)")
  44   {
  45     // 5 choose 0 = 1 test
  46     REQUIRE_NOTHROW(Configuration({&e1}));
  47
  48     // 5 choose 1 = 5 tests
  49     REQUIRE_THROWS_AS(Configuration({&e2}), std::invalid_argument);
  50     REQUIRE_THROWS_AS(Configuration({&e3}), std::invalid_argument);
  51     REQUIRE_THROWS_AS(Configuration({&e4}), std::invalid_argument);
  52     REQUIRE_THROWS_AS(Configuration({&e5}), std::invalid_argument);
  53
  54     // 5 choose 2 = 10 tests
  55     REQUIRE_NOTHROW(Configuration({&e1, &e2}));
  56     REQUIRE_THROWS_AS(Configuration({&e1, &e3}), std::invalid_argument);
  57     REQUIRE_THROWS_AS(Configuration({&e1, &e4}), std::invalid_argument);
  58     REQUIRE_THROWS_AS(Configuration({&e1, &e5}), std::invalid_argument);
  59     REQUIRE_THROWS_AS(Configuration({&e2, &e3}), std::invalid_argument);
  60     REQUIRE_THROWS_AS(Configuration({&e2, &e4}), std::invalid_argument);
  61     REQUIRE_THROWS_AS(Configuration({&e2, &e5}), std::invalid_argument);
  62     REQUIRE_THROWS_AS(Configuration({&e3, &e4}), std::invalid_argument);
  63     REQUIRE_THROWS_AS(Configuration({&e3, &e5}), std::invalid_argument);
  64     REQUIRE_THROWS_AS(Configuration({&e4, &e5}), std::invalid_argument);
  65
  66     // 5 choose 3 = 10 tests
  67     REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}));
  68     REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4}), std::invalid_argument);
  69     REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e5}), std::invalid_argument);
  70     REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4}), std::invalid_argument);
  71     REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e5}), std::invalid_argument);
  72     REQUIRE_THROWS_AS(Configuration({&e1, &e4, &e5}), std::invalid_argument);
  73     REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4}), std::invalid_argument);
  74     REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e5}), std::invalid_argument);
  75     REQUIRE_THROWS_AS(Configuration({&e2, &e4, &e5}), std::invalid_argument);
  76     REQUIRE_THROWS_AS(Configuration({&e3, &e4, &e5}), std::invalid_argument);
  77
  78     // 5 choose 4 = 5 tests
  79     REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}));
  80     REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e5}));
  81     REQUIRE_THROWS_AS(Configuration({&e1, &e2, &e4, &e5}), std::invalid_argument);
  82     REQUIRE_THROWS_AS(Configuration({&e1, &e3, &e4, &e5}), std::invalid_argument);
  83     REQUIRE_THROWS_AS(Configuration({&e2, &e3, &e4, &e5}), std::invalid_argument);
  84
  85     // 5 choose 5 = 1 test
  86     REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4, &e5}));
  87   }
  88 }
  89
  90 TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events")
  91 {
  92   // The following tests concern the given event structure:
  93   //                e1
  94   //              /
  95   //            e2
  96   //           /
  97   //         /  /
  98   //        e3   e4
  99   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
 100   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
 101   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
 102   UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(3));
 103
 104   REQUIRE_THROWS_AS(Configuration().add_event(nullptr), std::invalid_argument);
 105   REQUIRE_THROWS_AS(Configuration().add_event(&e2), std::invalid_argument);
 106   REQUIRE_THROWS_AS(Configuration().add_event(&e3), std::invalid_argument);
 107   REQUIRE_THROWS_AS(Configuration().add_event(&e4), std::invalid_argument);
 108   REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e3), std::invalid_argument);
 109   REQUIRE_THROWS_AS(Configuration({&e1}).add_event(&e4), std::invalid_argument);
 110
 111   REQUIRE_NOTHROW(Configuration().add_event(&e1));
 112   REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e1));
 113   REQUIRE_NOTHROW(Configuration({&e1}).add_event(&e2));
 114   REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e1));
 115   REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e2));
 116   REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e3));
 117   REQUIRE_NOTHROW(Configuration({&e1, &e2}).add_event(&e4));
 118   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e1));
 119   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e2));
 120   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e3));
 121   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3}).add_event(&e4));
 122   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e1));
 123   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e2));
 124   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e3));
 125   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e4}).add_event(&e4));
 126   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e1));
 127   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e2));
 128   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e3));
 129   REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4}).add_event(&e4));
 130 }
 131
 132 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order")
 133 {
 134   // The following tests concern the given event structure:
 135   //               e1
 136   //              /
 137   //            e2
 138   //           /
 139   //          e3
 140   //         /
 141   //        e4
 142   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
 143   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
 144   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(3));
 145   UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(4));
 146
 147   SECTION("Topological ordering for entire set")
 148   {
 149     Configuration C{&e1, &e2, &e3, &e4};
 150     REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
 151     REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 152             std::vector<const UnfoldingEvent*>{&e4, &e3, &e2, &e1});
 153   }
 154
 155   SECTION("Topological ordering for subsets")
 156   {
 157     SECTION("No elements")
 158     {
 159       Configuration C;
 160       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
 161       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
 162     }
 163
 164     SECTION("e1 only")
 165     {
 166       Configuration C{&e1};
 167       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
 168       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
 169     }
 170
 171     SECTION("e1 and e2 only")
 172     {
 173       Configuration C{&e1, &e2};
 174       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
 175       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
 176     }
 177
 178     SECTION("e1, e2, and e3 only")
 179     {
 180       Configuration C{&e1, &e2, &e3};
 181       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
 182       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 183               std::vector<const UnfoldingEvent*>{&e3, &e2, &e1});
 184     }
 185   }
 186 }
 187
 188 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Complicated")
 189 {
 190   // The following tests concern the given event structure:
 191   //                e1
 192   //              /
 193   //            e2
 194   //           /
 195   //          e3
 196   //         /  /
 197   //        e4   e6
 198   //        /
 199   //       e5
 200   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
 201   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
 202   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(3));
 203   UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(4));
 204   UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>(5));
 205   UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>(6));
 206
 207   SECTION("Topological ordering for subsets")
 208   {
 209     SECTION("No elements")
 210     {
 211       Configuration C;
 212       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{});
 213       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{});
 214     }
 215
 216     SECTION("e1 only")
 217     {
 218       Configuration C{&e1};
 219       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1});
 220       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e1});
 221     }
 222
 223     SECTION("e1 and e2 only")
 224     {
 225       Configuration C{&e1, &e2};
 226       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2});
 227       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() == std::vector<const UnfoldingEvent*>{&e2, &e1});
 228     }
 229
 230     SECTION("e1, e2, and e3 only")
 231     {
 232       Configuration C{&e1, &e2, &e3};
 233       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3});
 234       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 235               std::vector<const UnfoldingEvent*>{&e3, &e2, &e1});
 236     }
 237
 238     SECTION("e1, e2, e3, and e6 only")
 239     {
 240       Configuration C{&e1, &e2, &e3, &e6};
 241       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6});
 242       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 243               std::vector<const UnfoldingEvent*>{&e6, &e3, &e2, &e1});
 244     }
 245
 246     SECTION("e1, e2, e3, and e4 only")
 247     {
 248       Configuration C{&e1, &e2, &e3, &e4};
 249       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4});
 250       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 251               std::vector<const UnfoldingEvent*>{&e4, &e3, &e2, &e1});
 252     }
 253
 254     SECTION("e1, e2, e3, e4, and e5 only")
 255     {
 256       Configuration C{&e1, &e2, &e3, &e4, &e5};
 257       REQUIRE(C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5});
 258       REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 259               std::vector<const UnfoldingEvent*>{&e5, &e4, &e3, &e2, &e1});
 260     }
 261
 262     SECTION("e1, e2, e3, e4 and e6 only")
 263     {
 264       // In this case, e4 and e6 are interchangeable. Hence, we have to check
 265       // if the sorting gives us *any* of the combinations
 266       Configuration C{&e1, &e2, &e3, &e4, &e6};
 267       REQUIRE((C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6} ||
 268                C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4}));
 269       REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
 270                    std::vector<const UnfoldingEvent*>{&e6, &e4, &e3, &e2, &e1} ||
 271                C.get_topologically_sorted_events_of_reverse_graph() ==
 272                    std::vector<const UnfoldingEvent*>{&e4, &e6, &e3, &e2, &e1}));
 273     }
 274
 275     SECTION("Topological ordering for entire set")
 276     {
 277       // In this case, e4/e5 are both interchangeable with e6. Hence, again we have to check
 278       // if the sorting gives us *any* of the combinations
 279       Configuration C{&e1, &e2, &e3, &e4, &e5, &e6};
 280       REQUIRE(
 281           (C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e5, &e6} ||
 282            C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e4, &e6, &e5} ||
 283            C.get_topologically_sorted_events() == std::vector<const UnfoldingEvent*>{&e1, &e2, &e3, &e6, &e4, &e5}));
 284       REQUIRE((C.get_topologically_sorted_events_of_reverse_graph() ==
 285                    std::vector<const UnfoldingEvent*>{&e6, &e5, &e4, &e3, &e2, &e1} ||
 286                C.get_topologically_sorted_events_of_reverse_graph() ==
 287                    std::vector<const UnfoldingEvent*>{&e5, &e6, &e4, &e3, &e2, &e1} ||
 288                C.get_topologically_sorted_events_of_reverse_graph() ==
 289                    std::vector<const UnfoldingEvent*>{&e5, &e4, &e6, &e3, &e2, &e1}));
 290     }
 291   }
 292 }
 293
 294 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Complicated")
 295 {
 296   // The following tests concern the given event structure:
 297   //                e1
 298   //              /   /
 299   //            e2    e8
 300   //           /  /    /  /
 301   //          e3   /   /    /
 302   //         /  /    /      e11
 303   //        e4  e6   e7
 304   //        /   /  /   /
 305   //       e5   e9    e10
 306   //        /   /     /
 307   //         /  /   /
 308   //         [   e12    ]
 309   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
 310   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
 311   UnfoldingEvent e8(EventSet({&e1}), std::make_shared<IndependentAction>(3));
 312   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(4));
 313   UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(5));
 314   UnfoldingEvent e5(EventSet({&e4}), std::make_shared<IndependentAction>(6));
 315   UnfoldingEvent e6(EventSet({&e4}), std::make_shared<IndependentAction>(7));
 316   UnfoldingEvent e7(EventSet({&e2, &e8}), std::make_shared<IndependentAction>(8));
 317   UnfoldingEvent e9(EventSet({&e6, &e7}), std::make_shared<IndependentAction>(9));
 318   UnfoldingEvent e10(EventSet({&e7}), std::make_shared<IndependentAction>(10));
 319   UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>(11));
 320   UnfoldingEvent e12(EventSet({&e5, &e9, &e10}), std::make_shared<IndependentAction>(12));
 321   Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12};
 322
 323   SECTION("Test every combination of the maximal configuration (forward graph)")
 324   {
 325     // To test this, we ensure that for the `i`th event
 326     // in `ordered_events`, each event in `ordered_events[0...<i]
 327     // is contained in the history of `ordered_events[i]`.
 328     EventSet events_seen;
 329     const auto ordered_events = C.get_topologically_sorted_events();
 330
 331     std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
 332       History history(e);
 333       for (const auto* e_hist : history) {
 334         // In this demo, we want to make sure that
 335         // we don't mark not yet seeing `e` as an error.
 336         // The history of `e` traverses `e` itself. All
 337         // other events in e's history are included in
 338         if (e_hist == e)
 339           continue;
 340
 341         // If this event has not been "seen" before,
 342         // this implies that event `e` appears earlier
 343         // in the list than one of its dependencies
 344         REQUIRE(events_seen.contains(e_hist));
 345       }
 346       events_seen.insert(e);
 347     });
 348   }
 349
 350   SECTION("Test every combination of the maximal configuration (reverse graph)")
 351   {
 352     // To test this, we ensure that for the `i`th event
 353     // in `ordered_events`, no event in `ordered_events[0...<i]
 354     // is contained in the history of `ordered_events[i]`.
 355     EventSet events_seen;
 356     const auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
 357
 358     std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
 359       History history(e);
 360
 361       for (const auto* e_hist : history) {
 362         // Unlike the test above, we DO want to ensure
 363         // that `e` itself ALSO isn't yet seen
 364
 365         // If this event has been "seen" before,
 366         // this implies that event `e` appears later
 367         // in the list than one of its ancestors
 368         REQUIRE_FALSE(events_seen.contains(e_hist));
 369       }
 370       events_seen.insert(e);
 371     });
 372   }
 373
 374   SECTION("Test that the topological ordering contains only the events of the configuration")
 375   {
 376     const EventSet events_seen = C.get_events();
 377
 378     SECTION("Forward direction")
 379     {
 380       auto ordered_events              = C.get_topologically_sorted_events();
 381       const EventSet ordered_event_set = EventSet(std::move(ordered_events));
 382       REQUIRE(events_seen == ordered_event_set);
 383     }
 384
 385     SECTION("Reverse direction")
 386     {
 387       auto ordered_events              = C.get_topologically_sorted_events_of_reverse_graph();
 388       const EventSet ordered_event_set = EventSet(std::move(ordered_events));
 389       REQUIRE(events_seen == ordered_event_set);
 390     }
 391   }
 392
 393   SECTION("Test that the topological ordering is equivalent to that of the configuration's events")
 394   {
 395     REQUIRE(C.get_topologically_sorted_events() == C.get_events().get_topological_ordering());
 396     REQUIRE(C.get_topologically_sorted_events_of_reverse_graph() ==
 397             C.get_events().get_topological_ordering_of_reverse_graph());
 398   }
 399 }
 400
 401 TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Basic Testing of Maximal Subsets")
 402 {
 403   // The following tests concern the given event structure:
 404   //                e1
 405   //              /   /
 406   //             e2   e5
 407   //            /     /
 408   //           e3    e6
 409   //           /     / /
 410   //          e4    e7 e8
 411   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(0));
 412   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(1));
 413   UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>(2));
 414   UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>(3));
 415   UnfoldingEvent e5(EventSet({&e1}), std::make_shared<IndependentAction>(4));
 416   UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>(5));
 417   UnfoldingEvent e7(EventSet({&e6}), std::make_shared<IndependentAction>(6));
 418   UnfoldingEvent e8(EventSet({&e6}), std::make_shared<IndependentAction>(7));
 419
 420   SECTION("Iteration over an empty configuration yields only the empty set")
 421   {
 422     Configuration C;
 423     maximal_subsets_iterator first(C);
 424     maximal_subsets_iterator last;
 425
 426     REQUIRE(*first == EventSet());
 427     ++first;
 428     REQUIRE(first == last);
 429   }
 430
 431   SECTION("Check counts of maximal event sets discovered")
 432   {
 433     std::unordered_map<int, int> maximal_subset_counts;
 434
 435     Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
 436     maximal_subsets_iterator first(C);
 437     maximal_subsets_iterator last;
 438
 439     for (; first != last; ++first) {
 440       maximal_subset_counts[(*first).size()]++;
 441     }
 442
 443     // First, ensure that there are only sets of size 0, 1, 2, and 3
 444     CHECK(maximal_subset_counts.size() == 4);
 445
 446     // The empty set should appear only once
 447     REQUIRE(maximal_subset_counts[0] == 1);
 448
 449     // 8 is the number of nodes in the graph
 450     REQUIRE(maximal_subset_counts[1] == 8);
 451
 452     // 13 = 3 * 4 (each of the left branch can combine with one in the right branch) + 1 (e7 + e8)
 453     REQUIRE(maximal_subset_counts[2] == 13);
 454
 455     // e7 + e8 must be included, so that means we can combine from the left branch
 456     REQUIRE(maximal_subset_counts[3] == 3);
 457   }
 458
 459   SECTION("Check counts of maximal event sets discovered with a filter")
 460   {
 461     std::unordered_map<int, int> maximal_subset_counts;
 462
 463     Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
 464
 465     SECTION("Filter with events part of initial maximal set")
 466     {
 467       EventSet interesting_bunch{&e2, &e4, &e7, &e8};
 468
 469       maximal_subsets_iterator first(
 470           C, [&interesting_bunch](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
 471       maximal_subsets_iterator last;
 472
 473       for (; first != last; ++first) {
 474         const auto& event_set = *first;
 475         // Only events in `interesting_bunch` can appear: thus no set
 476         // should include anything else other than `interesting_bunch`
 477         REQUIRE(event_set.is_subset_of(interesting_bunch));
 478         REQUIRE(event_set.is_maximal());
 479         maximal_subset_counts[event_set.size()]++;
 480       }
 481
 482       // The empty set should (still) appear only once
 483       REQUIRE(maximal_subset_counts[0] == 1);
 484
 485       // 4 is the number of nodes in the `interesting_bunch`
 486       REQUIRE(maximal_subset_counts[1] == 4);
 487
 488       // 5 = 2 * 2 (each of the left branch can combine with one in the right branch) + 1 (e7 + e8)
 489       REQUIRE(maximal_subset_counts[2] == 5);
 490
 491       // e7 + e8 must be included, so that means we can combine from the left branch (only e2 and e4)
 492       REQUIRE(maximal_subset_counts[3] == 2);
 493
 494       // There are no subsets of size 4 (or higher, but that
 495       // is tested by asserting each maximal set traversed is a subset)
 496       REQUIRE(maximal_subset_counts[4] == 0);
 497     }
 498
 499     SECTION("Filter with interesting subset not initially part of the maximal set")
 500     {
 501       EventSet interesting_bunch{&e3, &e5, &e6};
 502
 503       maximal_subsets_iterator first(
 504           C, [&interesting_bunch](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
 505       maximal_subsets_iterator last;
 506
 507       for (; first != last; ++first) {
 508         const auto& event_set = *first;
 509         // Only events in `interesting_bunch` can appear: thus no set
 510         // should include anything else other than `interesting_bunch`
 511         REQUIRE(event_set.is_subset_of(interesting_bunch));
 512         REQUIRE(event_set.is_maximal());
 513         maximal_subset_counts[event_set.size()]++;
 514       }
 515
 516       // The empty set should (still) appear only once
 517       REQUIRE(maximal_subset_counts[0] == 1);
 518
 519       // 3 is the number of nodes in the `interesting_bunch`
 520       REQUIRE(maximal_subset_counts[1] == 3);
 521
 522       // 2 = e3, e5 and e3, e6
 523       REQUIRE(maximal_subset_counts[2] == 2);
 524
 525       // There are no subsets of size 3 (or higher, but that
 526       // is tested by asserting each maximal set traversed is a subset)
 527       REQUIRE(maximal_subset_counts[3] == 0);
 528     }
 529   }
 530 }
 531
 532 TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal Subsets Iteration")
 533 {
 534   // The following tests concern the given event structure:
 535   //                              e1
 536   //                            /   /
 537   //                          e2    e3
 538   //                          / /   /  /
 539   //               +------* e4 *e5 e6  e7
 540   //               |        /   ///   /  /
 541   //               |       e8   e9    e10
 542   //               |      /  /   /\      /
 543   //               |   e11 e12 e13 e14   e15
 544   //               |   /      / / /   /  /
 545   //               +-> e16     e17     e18
 546   UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(1));
 547   UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(2));
 548   UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(3));
 549   UnfoldingEvent e4(EventSet({&e2}), std::make_shared<IndependentAction>(4));
 550   UnfoldingEvent e5(EventSet({&e2}), std::make_shared<IndependentAction>(5));
 551   UnfoldingEvent e6(EventSet({&e3}), std::make_shared<IndependentAction>(6));
 552   UnfoldingEvent e7(EventSet({&e3}), std::make_shared<IndependentAction>(7));
 553   UnfoldingEvent e8(EventSet({&e4}), std::make_shared<IndependentAction>(8));
 554   UnfoldingEvent e9(EventSet({&e4, &e5, &e6}), std::make_shared<IndependentAction>(9));
 555   UnfoldingEvent e10(EventSet({&e6, &e7}), std::make_shared<IndependentAction>(10));
 556   UnfoldingEvent e11(EventSet({&e8}), std::make_shared<IndependentAction>(11));
 557   UnfoldingEvent e12(EventSet({&e8}), std::make_shared<IndependentAction>(12));
 558   UnfoldingEvent e13(EventSet({&e9}), std::make_shared<IndependentAction>(13));
 559   UnfoldingEvent e14(EventSet({&e9}), std::make_shared<IndependentAction>(14));
 560   UnfoldingEvent e15(EventSet({&e10}), std::make_shared<IndependentAction>(15));
 561   UnfoldingEvent e16(EventSet({&e5, &e11}), std::make_shared<IndependentAction>(16));
 562   UnfoldingEvent e17(EventSet({&e12, &e13, &e14}), std::make_shared<IndependentAction>(17));
 563   UnfoldingEvent e18(EventSet({&e14, &e15}), std::make_shared<IndependentAction>(18));
 564   Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8, &e9, &e10, &e11, &e12, &e13, &e14, &e15, &e16, &e17, &e18};
 565
 566   SECTION("Every subset iterated over is maximal")
 567   {
 568     maximal_subsets_iterator first(C);
 569     maximal_subsets_iterator last;
 570
 571     // Make sure we actually have something to iterate over
 572     REQUIRE(first != last);
 573
 574     for (; first != last; ++first) {
 575       REQUIRE((*first).size() <= C.get_events().size());
 576       REQUIRE((*first).is_maximal());
 577     }
 578   }
 579
 580   SECTION("Test that the maximal set ordering is equivalent to that of the configuration's events")
 581   {
 582     maximal_subsets_iterator first_config(C);
 583     maximal_subsets_iterator first_events(C.get_events());
 584     maximal_subsets_iterator last;
 585
 586     // Make sure we actually have something to iterate over
 587     REQUIRE(first_config != last);
 588     REQUIRE(first_config == first_events);
 589     REQUIRE(first_events != last);
 590
 591     for (; first_config != last; ++first_config, ++first_events) {
 592       // first_events and first_config should always be at the same location
 593       REQUIRE(first_events != last);
 594       const auto& first_config_set = *first_config;
 595       const auto& first_events_set = *first_events;
 596
 597       REQUIRE(first_config_set.size() <= C.get_events().size());
 598       REQUIRE(first_config_set.is_maximal());
 599       REQUIRE(first_events_set == first_config_set);
 600     }
 601
 602     // Iteration with events directly should now also be finished
 603     REQUIRE(first_events == last);
 604   }
 605 }
 606
 607 TEST_CASE("simgrid::mc::udpor::Configuration: Latest Transitions")
 608 {
 609   // The following tests concern the given event structure (labeled as "event(actor)")
 610   //                  e1(1)
 611   //                 /     /
 612   //              e2(1)   e3(2)
 613   //              /    //     /
 614   //            e4(3) e5(2)  e6(1)
 615   //                  /   /
 616   //               e7(1) e8(1)
 617   const auto t1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 618   const auto t2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 619   const auto t3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 620   const auto t4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
 621   const auto t5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 622   const auto t6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 623   const auto t7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 624   const auto t8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 625
 626   const UnfoldingEvent e1(EventSet(), t1);
 627   const UnfoldingEvent e2(EventSet({&e1}), t2);
 628   const UnfoldingEvent e3(EventSet({&e1}), t3);
 629   const UnfoldingEvent e4(EventSet({&e2}), t4);
 630   const UnfoldingEvent e5(EventSet({&e2, &e3}), t5);
 631   const UnfoldingEvent e6(EventSet({&e3}), t6);
 632   const UnfoldingEvent e7(EventSet({&e5}), t7);
 633   const UnfoldingEvent e8(EventSet({&e5}), t8);
 634
 635   SECTION("Test that the latest events are correct on initialization")
 636   {
 637     SECTION("Empty configuration has no events")
 638     {
 639       Configuration C;
 640       REQUIRE_FALSE(C.get_latest_event_of(1).has_value());
 641       REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 642       REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 643
 644       REQUIRE_FALSE(C.get_latest_action_of(1).has_value());
 645       REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 646       REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 647     }
 648
 649     SECTION("Missing two actors")
 650     {
 651       Configuration C{&e1};
 652       REQUIRE(C.get_latest_event_of(1).has_value());
 653       REQUIRE(C.get_latest_event_of(1).value() == &e1);
 654
 655       REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 656       REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 657
 658       REQUIRE(C.get_latest_action_of(1).has_value());
 659       REQUIRE(C.get_latest_action_of(1).value() == t1.get());
 660
 661       REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 662       REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 663     }
 664
 665     SECTION("Two events with one actor yields the latest event")
 666     {
 667       Configuration C{&e1, &e2};
 668       REQUIRE(C.get_latest_event_of(1).has_value());
 669       REQUIRE(C.get_latest_event_of(1).value() == &e2);
 670
 671       REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 672       REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 673
 674       REQUIRE(C.get_latest_action_of(1).has_value());
 675       REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 676
 677       REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 678       REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 679     }
 680
 681     SECTION("Two events with two actors")
 682     {
 683       Configuration C{&e1, &e3};
 684       REQUIRE(C.get_latest_event_of(1).has_value());
 685       REQUIRE(C.get_latest_event_of(1).value() == &e1);
 686
 687       REQUIRE(C.get_latest_event_of(2).has_value());
 688       REQUIRE(C.get_latest_event_of(2).value() == &e3);
 689
 690       REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 691
 692       REQUIRE(C.get_latest_action_of(1).has_value());
 693       REQUIRE(C.get_latest_action_of(1).value() == t1.get());
 694
 695       REQUIRE(C.get_latest_action_of(2).has_value());
 696       REQUIRE(C.get_latest_action_of(2).value() == t3.get());
 697
 698       REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 699     }
 700
 701     SECTION("Three different actors actors")
 702     {
 703       Configuration C{&e1, &e2, &e3, &e4, &e5};
 704       REQUIRE(C.get_latest_event_of(1).has_value());
 705       REQUIRE(C.get_latest_event_of(1).value() == &e2);
 706
 707       REQUIRE(C.get_latest_event_of(2).has_value());
 708       REQUIRE(C.get_latest_event_of(2).value() == &e5);
 709
 710       REQUIRE(C.get_latest_event_of(3).has_value());
 711       REQUIRE(C.get_latest_event_of(3).value() == &e4);
 712
 713       REQUIRE(C.get_latest_action_of(1).has_value());
 714       REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 715
 716       REQUIRE(C.get_latest_action_of(2).has_value());
 717       REQUIRE(C.get_latest_action_of(2).value() == t5.get());
 718
 719       REQUIRE(C.get_latest_action_of(3).has_value());
 720       REQUIRE(C.get_latest_action_of(3).value() == t4.get());
 721     }
 722   }
 723
 724   SECTION("Test that the latest events are correct when adding new events")
 725   {
 726     Configuration C;
 727     REQUIRE_FALSE(C.get_latest_event_of(1).has_value());
 728     REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 729     REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 730     REQUIRE_FALSE(C.get_latest_action_of(1).has_value());
 731     REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 732     REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 733
 734     C.add_event(&e1);
 735     REQUIRE(C.get_latest_event_of(1).has_value());
 736     REQUIRE(C.get_latest_event_of(1).value() == &e1);
 737     REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 738     REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 739     REQUIRE(C.get_latest_action_of(1).has_value());
 740     REQUIRE(C.get_latest_action_of(1).value() == t1.get());
 741     REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 742     REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 743
 744     C.add_event(&e2);
 745     REQUIRE(C.get_latest_event_of(1).has_value());
 746     REQUIRE(C.get_latest_event_of(1).value() == &e2);
 747     REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
 748     REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 749     REQUIRE(C.get_latest_action_of(1).has_value());
 750     REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 751     REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
 752     REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 753
 754     C.add_event(&e3);
 755     REQUIRE(C.get_latest_event_of(1).has_value());
 756     REQUIRE(C.get_latest_event_of(1).value() == &e2);
 757     REQUIRE(C.get_latest_event_of(2).has_value());
 758     REQUIRE(C.get_latest_event_of(2).value() == &e3);
 759     REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
 760     REQUIRE(C.get_latest_action_of(1).has_value());
 761     REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 762     REQUIRE(C.get_latest_action_of(2).has_value());
 763     REQUIRE(C.get_latest_action_of(2).value() == t3.get());
 764     REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
 765
 766     C.add_event(&e4);
 767     REQUIRE(C.get_latest_event_of(1).has_value());
 768     REQUIRE(C.get_latest_event_of(1).value() == &e2);
 769     REQUIRE(C.get_latest_event_of(2).has_value());
 770     REQUIRE(C.get_latest_event_of(2).value() == &e3);
 771     REQUIRE(C.get_latest_event_of(3).has_value());
 772     REQUIRE(C.get_latest_event_of(3).value() == &e4);
 773     REQUIRE(C.get_latest_action_of(1).has_value());
 774     REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 775     REQUIRE(C.get_latest_action_of(2).has_value());
 776     REQUIRE(C.get_latest_action_of(2).value() == t3.get());
 777     REQUIRE(C.get_latest_action_of(3).has_value());
 778     REQUIRE(C.get_latest_action_of(3).value() == t4.get());
 779
 780     C.add_event(&e5);
 781     REQUIRE(C.get_latest_event_of(1).has_value());
 782     REQUIRE(C.get_latest_event_of(1).value() == &e2);
 783     REQUIRE(C.get_latest_event_of(2).has_value());
 784     REQUIRE(C.get_latest_event_of(2).value() == &e5);
 785     REQUIRE(C.get_latest_event_of(3).has_value());
 786     REQUIRE(C.get_latest_event_of(3).value() == &e4);
 787     REQUIRE(C.get_latest_action_of(1).has_value());
 788     REQUIRE(C.get_latest_action_of(1).value() == t2.get());
 789     REQUIRE(C.get_latest_action_of(2).has_value());
 790     REQUIRE(C.get_latest_action_of(2).value() == t5.get());
 791     REQUIRE(C.get_latest_action_of(3).has_value());
 792     REQUIRE(C.get_latest_action_of(3).value() == t4.get());
 793   }
 794 }
 795
 796 TEST_CASE("simgrid::mc::udpor::Configuration: Computing Full Alternatives in Reader/Writer Example")
 797 {
 798   // The following tests concern the given event structure that is given as
 799   // an example in figure 1 of the original UDPOR paper.
 800   //                  e0
 801   //              /  /   /
 802   //            e1   e4   e7
 803   //           /     /  //   /
 804   //         /  /   e5  e8   e9
 805   //        e2 e3   /        /
 806   //               e6       e10
 807   //
 808   // Theses tests walk through exactly the configurations and sets of `D` that
 809   // UDPOR COULD encounter as it walks through the unfolding. Note that
 810   // if there are multiple alternatives to any given configuration, UDPOR can
 811   // continue searching any one of them. The sequence assumes UDPOR first picks `e1`,
 812   // then `e4`, and then `e7`
 813   Unfolding U;
 814
 815   auto e0 = std::make_unique<UnfoldingEvent>(
 816       EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
 817   auto* e0_handle = e0.get();
 818
 819   auto e1        = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}),
 820                                              std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
 821   auto* e1_handle = e1.get();
 822
 823   auto e2 = std::make_unique<UnfoldingEvent>(
 824       EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
 825   auto* e2_handle = e2.get();
 826
 827   auto e3 = std::make_unique<UnfoldingEvent>(
 828       EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
 829   auto* e3_handle = e3.get();
 830
 831   auto e4 = std::make_unique<UnfoldingEvent>(
 832       EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
 833   auto* e4_handle = e4.get();
 834
 835   auto e5        = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}),
 836                                              std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
 837   auto* e5_handle = e5.get();
 838
 839   auto e6 = std::make_unique<UnfoldingEvent>(
 840       EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
 841   auto* e6_handle = e6.get();
 842
 843   auto e7 = std::make_unique<UnfoldingEvent>(
 844       EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
 845   auto* e7_handle = e7.get();
 846
 847   auto e8        = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}),
 848                                              std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
 849   auto* e8_handle = e8.get();
 850
 851   auto e9        = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}),
 852                                              std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
 853   auto* e9_handle = e9.get();
 854
 855   auto e10 = std::make_unique<UnfoldingEvent>(
 856       EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
 857   auto* e10_handle = e10.get();
 858
 859   SECTION("Alternative computation call 1")
 860   {
 861     // During the first call to Alt(C, D + {e}),
 862     // UDPOR believes `U` to be the following:
 863     //
 864     //                  e0
 865     //              /  /   /
 866     //            e1   e4   e7
 867     //           /
 868     //         /  /
 869     //        e2 e3
 870     //
 871     // C := {e0, e1, e2} and `Explore(C, D, A)` picked `e3`
 872     // (since en(C') where C' := {e0, e1, e2, e3} is empty
 873     // [so UDPOR will simply return when C' is reached])
 874     //
 875     // Thus the computation is (since D is empty at first)
 876     //
 877     // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3})
 878     //
 879     // where U is given above. There are no alternatives in
 880     // this case since `e4` and `e7` conflict with `e1` (so
 881     // they cannot be added to C to form a configuration)
 882     const Configuration C{e0_handle, e1_handle, e2_handle};
 883     const EventSet D_plus_e{e3_handle};
 884
 885     REQUIRE(U.empty());
 886     U.insert(std::move(e0));
 887     U.insert(std::move(e1));
 888     U.insert(std::move(e2));
 889     U.insert(std::move(e3));
 890     U.insert(std::move(e4));
 891     U.insert(std::move(e7));
 892
 893     const auto alternative = C.compute_alternative_to(D_plus_e, U);
 894     REQUIRE_FALSE(alternative.has_value());
 895   }
 896
 897   SECTION("Alternative computation call 2")
 898   {
 899     // During the second call to Alt(C, D + {e}),
 900     // UDPOR believes `U` to be the following:
 901     //
 902     //                  e0
 903     //              /  /   /
 904     //            e1   e4   e7
 905     //           /
 906     //         /  /
 907     //        e2 e3
 908     //
 909     // C := {e0, e1} and `Explore(C, D, A)` picked `e2`.
 910     //
 911     // Thus the computation is (since D is still empty)
 912     //
 913     // Alt(C, D + {e}) --> Alt({e0, e1}, {e2})
 914     //
 915     // where U is given above. There are no alternatives in
 916     // this case since `e4` and `e7` conflict with `e1` (so
 917     // they cannot be added to C to form a configuration) and
 918     // e3 is NOT in conflict with either e0 or e1
 919     const Configuration C{e0_handle, e1_handle};
 920     const EventSet D_plus_e{e2_handle};
 921
 922     REQUIRE(U.empty());
 923     U.insert(std::move(e0));
 924     U.insert(std::move(e1));
 925     U.insert(std::move(e2));
 926     U.insert(std::move(e3));
 927     U.insert(std::move(e4));
 928     U.insert(std::move(e7));
 929
 930     const auto alternative = C.compute_alternative_to(D_plus_e, U);
 931     REQUIRE_FALSE(alternative.has_value());
 932   }
 933
 934   SECTION("Alternative computation call 3")
 935   {
 936     // During the thrid call to Alt(C, D + {e}),
 937     // UDPOR believes `U` to be the following:
 938     //
 939     //                 e0
 940     //              /  /   /
 941     //            e1   e4   e7
 942     //           /
 943     //         /  /
 944     //        e2 e3
 945     //
 946     // C := {e0} and `Explore(C, D, A)` picked `e1`.
 947     //
 948     // Thus the computation is (since D is still empty)
 949     //
 950     // Alt(C, D + {e}) --> Alt({e0}, {e1})
 951     //
 952     // where U is given above. There are two alternatives in this case:
 953     // {e0, e4} and {e0, e7}. Either one would be a valid choice for
 954     // UDPOR, so we must check for the precense of either
 955     const Configuration C{e0_handle};
 956     const EventSet D_plus_e{e1_handle};
 957
 958     REQUIRE(U.empty());
 959     U.insert(std::move(e0));
 960     U.insert(std::move(e1));
 961     U.insert(std::move(e2));
 962     U.insert(std::move(e3));
 963     U.insert(std::move(e4));
 964     U.insert(std::move(e7));
 965
 966     const auto alternative = C.compute_alternative_to(D_plus_e, U);
 967     REQUIRE(alternative.has_value());
 968
 969     // The first alternative that is found is the one that is chosen. Since
 970     // traversal over the elements of an unordered_set<> are not guaranteed,
 971     // both {e0, e4} and {e0, e7} are valid alternatives
 972     REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e4_handle}) or
 973              alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
 974   }
 975
 976   SECTION("Alternative computation call 4")
 977   {
 978     // During the fourth call to Alt(C, D + {e}),
 979     // UDPOR believes `U` to be the following:
 980     //
 981     //                  e0
 982     //              /  /   /
 983     //            e1   e4   e7
 984     //           /     /  //
 985     //         /  /   e5  e8
 986     //        e2 e3   /
 987     //               e6
 988     //
 989     // C := {e0, e4, e5} and `Explore(C, D, A)` picked `e6`
 990     // (since en(C') where C' := {e0, e4, e5, e6} is empty
 991     // [so UDPOR will simply return when C' is reached])
 992     //
 993     // Thus the computation is (since D is {e1})
 994     //
 995     // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6})
 996     //
 997     // where U is given above. There are no alternatives in this
 998     // case, since:
 999     //
1000     // 1.`e2/e3` are eliminated since their histories contain `e1`
1001     // 2. `e7/e8` are eliminated because they conflict with `e5`
1002     const Configuration C{e0_handle, e4_handle, e5_handle};
1003     const EventSet D_plus_e{e1_handle, e6_handle};
1004
1005     REQUIRE(U.empty());
1006     U.insert(std::move(e0));
1007     U.insert(std::move(e1));
1008     U.insert(std::move(e2));
1009     U.insert(std::move(e3));
1010     U.insert(std::move(e4));
1011     U.insert(std::move(e6));
1012     U.insert(std::move(e7));
1013     U.insert(std::move(e8));
1014
1015     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1016     REQUIRE_FALSE(alternative.has_value());
1017   }
1018
1019   SECTION("Alternative computation call 5")
1020   {
1021     // During the fifth call to Alt(C, D + {e}),
1022     // UDPOR believes `U` to be the following:
1023     //
1024     //                  e0
1025     //              /  /   /
1026     //            e1   e4   e7
1027     //           /     /  //
1028     //         /  /   e5  e8
1029     //        e2 e3   /
1030     //               e6
1031     //
1032     // C := {e0, e4} and `Explore(C, D, A)` picked `e5`
1033     // (since en(C') where C' := {e0, e4, e5, e6} is empty
1034     // [so UDPOR will simply return when C' is reached])
1035     //
1036     // Thus the computation is (since D is {e1})
1037     //
1038     // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5})
1039     //
1040     // where U is given above. There are THREE alternatives in this case,
1041     // viz. {e0, e7}, {e0, e4, e7} and {e0, e4, e7, e8}.
1042     //
1043     // To continue the search, UDPOR computes J / C which in this
1044     // case gives {e7, e8}. Since `e8` is not in en(C), UDPOR will
1045     // choose `e7` next and add `e5` to `D`
1046     const Configuration C{e0_handle, e4_handle};
1047     const EventSet D_plus_e{e1_handle, e5_handle};
1048
1049     REQUIRE(U.empty());
1050     U.insert(std::move(e0));
1051     U.insert(std::move(e1));
1052     U.insert(std::move(e2));
1053     U.insert(std::move(e3));
1054     U.insert(std::move(e4));
1055     U.insert(std::move(e6));
1056     U.insert(std::move(e7));
1057     U.insert(std::move(e8));
1058     REQUIRE(U.size() == 8);
1059
1060     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1061     REQUIRE(alternative.has_value());
1062     REQUIRE((alternative.value().get_events() == EventSet({e0_handle, e7_handle}) or
1063              alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) or
1064              alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})));
1065   }
1066
1067   SECTION("Alternative computation call 6")
1068   {
1069     // During the sixth call to Alt(C, D + {e}),
1070     // UDPOR believes `U` to be the following:
1071     //
1072     //                 e0
1073     //              /  /   /
1074     //            e1   e4   e7
1075     //           /     /  //   /
1076     //         /  /   e5  e8   e9
1077     //        e2 e3   /
1078     //               e6
1079     //
1080     // C := {e0, e4, e7} and `Explore(C, D, A)` picked `e8`
1081     // (since en(C') where C' := {e0, e4, e7, e8} is empty
1082     // [so UDPOR will simply return when C' is reached])
1083     //
1084     // Thus the computation is (since D is {e1, e5} [see the last step])
1085     //
1086     // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8})
1087     //
1088     // where U is given above. There are no alternatives in this case
1089     // since all `e9` conflicts with `e4` and all other events of `U`
1090     // are eliminated since their history intersects `D`
1091     const Configuration C{e0_handle, e4_handle, e7_handle};
1092     const EventSet D_plus_e{e1_handle, e5_handle, e8_handle};
1093
1094     REQUIRE(U.empty());
1095     U.insert(std::move(e0));
1096     U.insert(std::move(e1));
1097     U.insert(std::move(e2));
1098     U.insert(std::move(e3));
1099     U.insert(std::move(e4));
1100     U.insert(std::move(e6));
1101     U.insert(std::move(e7));
1102     U.insert(std::move(e8));
1103     U.insert(std::move(e9));
1104
1105     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1106     REQUIRE_FALSE(alternative.has_value());
1107   }
1108
1109   SECTION("Alternative computation call 7")
1110   {
1111     // During the seventh call to Alt(C, D + {e}),
1112     // UDPOR believes `U` to be the following:
1113     //
1114     //                 e0
1115     //              /  /   /
1116     //            e1   e4   e7
1117     //           /     /  //   /
1118     //         /  /   e5  e8   e9
1119     //        e2 e3   /
1120     //               e6
1121     //
1122     // C := {e0, e4} and `Explore(C, D, A)` picked `e7`
1123     //
1124     // Thus the computation is (since D is {e1, e5} [see call 5])
1125     //
1126     // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7})
1127     //
1128     // where U is given above. There are no alternatives again in this case
1129     // since all `e9` conflicts with `e4` and all other events of `U`
1130     // are eliminated since their history intersects `D`
1131     const Configuration C{e0_handle, e4_handle};
1132     const EventSet D_plus_e{e1_handle, e5_handle, e7_handle};
1133
1134     REQUIRE(U.empty());
1135     U.insert(std::move(e0));
1136     U.insert(std::move(e1));
1137     U.insert(std::move(e2));
1138     U.insert(std::move(e3));
1139     U.insert(std::move(e4));
1140     U.insert(std::move(e6));
1141     U.insert(std::move(e7));
1142     U.insert(std::move(e8));
1143     U.insert(std::move(e9));
1144
1145     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1146     REQUIRE_FALSE(alternative.has_value());
1147   }
1148
1149   SECTION("Alternative computation call 8")
1150   {
1151     // During the eigth call to Alt(C, D + {e}),
1152     // UDPOR believes `U` to be the following:
1153     //
1154     //                 e0
1155     //              /  /   /
1156     //            e1   e4   e7
1157     //           /     /  //   /
1158     //         /  /   e5  e8   e9
1159     //        e2 e3   /
1160     //               e6
1161     //
1162     // C := {e0} and `Explore(C, D, A)` picked `e4`. At this
1163     // point, UDPOR finished its recursive search of {e0, e4}
1164     // after having finished {e0, e1} prior.
1165     //
1166     // Thus the computation is (since D = {e1})
1167     //
1168     // Alt(C, D + {e}) --> Alt({e0}, {e1, e4})
1169     //
1170     // where U is given above. There is one alternative in this
1171     // case, viz {e0, e7, e9} since
1172     // 1. e9 conflicts with e4 in D
1173     // 2. e7 conflicts with e1 in D
1174     // 3. the set {e7, e9} is conflict-free since `e7 < e9`
1175     // 4. all other events are eliminated since their histories
1176     // intersect D
1177     //
1178     // UDPOR will continue its recursive search following `e7`
1179     // and add `e4` to D
1180     const Configuration C{e0_handle};
1181     const EventSet D_plus_e{e1_handle, e4_handle};
1182
1183     REQUIRE(U.empty());
1184     U.insert(std::move(e0));
1185     U.insert(std::move(e1));
1186     U.insert(std::move(e2));
1187     U.insert(std::move(e3));
1188     U.insert(std::move(e4));
1189     U.insert(std::move(e6));
1190     U.insert(std::move(e7));
1191     U.insert(std::move(e8));
1192     U.insert(std::move(e9));
1193
1194     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1195     REQUIRE(alternative.has_value());
1196     REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
1197   }
1198
1199   SECTION("Alternative computation call 9")
1200   {
1201     // During the ninth call to Alt(C, D + {e}),
1202     // UDPOR believes `U` to be the following:
1203     //
1204     //                  e0
1205     //              /  /   /
1206     //            e1   e4   e7
1207     //           /     /  //   /
1208     //         /  /   e5  e8   e9
1209     //        e2 e3   /        /
1210     //               e6       e10
1211     //
1212     // C := {e0, e7, e9} and `Explore(C, D, A)` picked `e10`.
1213     // (since en(C') where C' := {e0, e7, e9, e10} is empty
1214     // [so UDPOR will simply return when C' is reached]).
1215     //
1216     // Thus the computation is (since D = {e1, e4} [see the previous step])
1217     //
1218     // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10})
1219     //
1220     // where U is given above. There are no alternatives in this case
1221     const Configuration C{e0_handle, e7_handle, e9_handle};
1222     const EventSet D_plus_e{e1_handle, e4_handle, e10_handle};
1223
1224     REQUIRE(U.empty());
1225     U.insert(std::move(e0));
1226     U.insert(std::move(e1));
1227     U.insert(std::move(e2));
1228     U.insert(std::move(e3));
1229     U.insert(std::move(e4));
1230     U.insert(std::move(e6));
1231     U.insert(std::move(e7));
1232     U.insert(std::move(e8));
1233     U.insert(std::move(e9));
1234     U.insert(std::move(e10));
1235
1236     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1237     REQUIRE_FALSE(alternative.has_value());
1238   }
1239
1240   SECTION("Alternative computation call 10")
1241   {
1242     // During the tenth call to Alt(C, D + {e}),
1243     // UDPOR believes `U` to be the following:
1244     //
1245     //                  e0
1246     //              /  /   /
1247     //            e1   e4   e7
1248     //           /     /  //   /
1249     //         /  /   e5  e8   e9
1250     //        e2 e3   /        /
1251     //               e6       e10
1252     //
1253     // C := {e0, e7} and `Explore(C, D, A)` picked `e9`.
1254     //
1255     // Thus the computation is (since D = {e1, e4} [see call 8])
1256     //
1257     // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9})
1258     //
1259     // where U is given above. There are no alternatives in this case
1260     const Configuration C{e0_handle, e7_handle};
1261     const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
1262
1263     REQUIRE(U.empty());
1264     U.insert(std::move(e0));
1265     U.insert(std::move(e1));
1266     U.insert(std::move(e2));
1267     U.insert(std::move(e3));
1268     U.insert(std::move(e4));
1269     U.insert(std::move(e6));
1270     U.insert(std::move(e7));
1271     U.insert(std::move(e8));
1272     U.insert(std::move(e9));
1273     U.insert(std::move(e10));
1274
1275     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1276     REQUIRE_FALSE(alternative.has_value());
1277   }
1278
1279   SECTION("Alternative computation call 11 (final call)")
1280   {
1281     // During the eleventh and final call to Alt(C, D + {e}),
1282     // UDPOR believes `U` to be the following:
1283     //
1284     //                  e0
1285     //              /  /   /
1286     //            e1   e4   e7
1287     //           /     /  //   /
1288     //         /  /   e5  e8   e9
1289     //        e2 e3   /        /
1290     //               e6       e10
1291     //
1292     // C := {e0} and `Explore(C, D, A)` picked `e7`.
1293     //
1294     // Thus the computation is (since D = {e1, e4} [see call 8])
1295     //
1296     // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7})
1297     //
1298     // where U is given above. There are no alternatives in this case:
1299     // everyone is eliminated!
1300     const Configuration C{e0_handle, e7_handle};
1301     const EventSet D_plus_e{e1_handle, e4_handle, e9_handle};
1302
1303     REQUIRE(U.empty());
1304     U.insert(std::move(e0));
1305     U.insert(std::move(e1));
1306     U.insert(std::move(e2));
1307     U.insert(std::move(e3));
1308     U.insert(std::move(e4));
1309     U.insert(std::move(e6));
1310     U.insert(std::move(e7));
1311     U.insert(std::move(e8));
1312     U.insert(std::move(e9));
1313     U.insert(std::move(e10));
1314
1315     const auto alternative = C.compute_alternative_to(D_plus_e, U);
1316     REQUIRE_FALSE(alternative.has_value());
1317   }
1318
1319   SECTION("Alternative computation next")
1320   {
1321     SECTION("Followed {e0, e7} first")
1322     {
1323       const EventSet D{e1_handle, e7_handle};
1324       const Configuration C{e0_handle};
1325
1326       REQUIRE(U.empty());
1327       U.insert(std::move(e0));
1328       U.insert(std::move(e1));
1329       U.insert(std::move(e2));
1330       U.insert(std::move(e3));
1331       U.insert(std::move(e4));
1332       U.insert(std::move(e5));
1333       U.insert(std::move(e7));
1334       U.insert(std::move(e8));
1335       U.insert(std::move(e9));
1336       U.insert(std::move(e10));
1337
1338       const auto alternative = C.compute_alternative_to(D, U);
1339       REQUIRE(alternative.has_value());
1340
1341       // In this case, only {e0, e4} is a valid alternative
1342       REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle}));
1343     }
1344
1345     SECTION("Followed {e0, e4} first")
1346     {
1347       const EventSet D{e1_handle, e4_handle};
1348       const Configuration C{e0_handle};
1349
1350       REQUIRE(U.empty());
1351       U.insert(std::move(e0));
1352       U.insert(std::move(e1));
1353       U.insert(std::move(e2));
1354       U.insert(std::move(e3));
1355       U.insert(std::move(e4));
1356       U.insert(std::move(e5));
1357       U.insert(std::move(e6));
1358       U.insert(std::move(e7));
1359       U.insert(std::move(e8));
1360       U.insert(std::move(e9));
1361
1362       const auto alternative = C.compute_alternative_to(D, U);
1363       REQUIRE(alternative.has_value());
1364
1365       // In this case, only {e0, e7} is a valid alternative
1366       REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));
1367     }
1368   }
1369 }