1 /* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
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. */
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"
15 #include <unordered_map>
17 using namespace simgrid::mc;
18 using namespace simgrid::mc::udpor;
20 TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
22 // The following tests concern the given event structure:
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));
36 SECTION("Creating a configuration without events")
39 REQUIRE(C.get_events().empty());
40 REQUIRE(C.get_latest_event() == nullptr);
43 SECTION("Creating a configuration with events (test violation of being causally closed)")
45 // 5 choose 0 = 1 test
46 REQUIRE_NOTHROW(Configuration({&e1}));
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);
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);
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);
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);
85 // 5 choose 5 = 1 test
86 REQUIRE_NOTHROW(Configuration({&e1, &e2, &e3, &e4, &e5}));
90 TEST_CASE("simgrid::mc::udpor::Configuration: Adding Events")
92 // The following tests concern the given event structure:
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));
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);
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));
132 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order")
134 // The following tests concern the given event structure:
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));
147 SECTION("Topological ordering for entire set")
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});
155 SECTION("Topological ordering for subsets")
157 SECTION("No elements")
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*>{});
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});
171 SECTION("e1 and e2 only")
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});
178 SECTION("e1, e2, and e3 only")
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});
188 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order More Complicated")
190 // The following tests concern the given event structure:
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));
207 SECTION("Topological ordering for subsets")
209 SECTION("No elements")
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*>{});
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});
223 SECTION("e1 and e2 only")
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});
230 SECTION("e1, e2, and e3 only")
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});
238 SECTION("e1, e2, e3, and e6 only")
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});
246 SECTION("e1, e2, e3, and e4 only")
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});
254 SECTION("e1, e2, e3, e4, and e5 only")
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});
262 SECTION("e1, e2, e3, e4 and e6 only")
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}));
275 SECTION("Topological ordering for entire set")
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};
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}));
294 TEST_CASE("simgrid::mc::udpor::Configuration: Topological Sort Order Very Complicated")
296 // The following tests concern the given event structure:
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};
323 SECTION("Test every combination of the maximal configuration (forward graph)")
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();
331 std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* 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
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));
346 events_seen.insert(e);
350 SECTION("Test every combination of the maximal configuration (reverse graph)")
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();
358 std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
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
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));
370 events_seen.insert(e);
374 SECTION("Test that the topological ordering contains only the events of the configuration")
376 const EventSet events_seen = C.get_events();
378 SECTION("Forward direction")
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);
385 SECTION("Reverse direction")
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);
393 SECTION("Test that the topological ordering is equivalent to that of the configuration's events")
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());
401 TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Basic Testing of Maximal Subsets")
403 // The following tests concern the given event structure:
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));
420 SECTION("Iteration over an empty configuration yields only the empty set")
423 maximal_subsets_iterator first(C);
424 maximal_subsets_iterator last;
426 REQUIRE(*first == EventSet());
428 REQUIRE(first == last);
431 SECTION("Check counts of maximal event sets discovered")
433 std::unordered_map<int, int> maximal_subset_counts;
435 Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
436 maximal_subsets_iterator first(C);
437 maximal_subsets_iterator last;
439 for (; first != last; ++first) {
440 maximal_subset_counts[(*first).size()]++;
443 // First, ensure that there are only sets of size 0, 1, 2, and 3
444 CHECK(maximal_subset_counts.size() == 4);
446 // The empty set should appear only once
447 REQUIRE(maximal_subset_counts[0] == 1);
449 // 8 is the number of nodes in the graph
450 REQUIRE(maximal_subset_counts[1] == 8);
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);
455 // e7 + e8 must be included, so that means we can combine from the left branch
456 REQUIRE(maximal_subset_counts[3] == 3);
459 SECTION("Check counts of maximal event sets discovered with a filter")
461 std::unordered_map<int, int> maximal_subset_counts;
463 Configuration C{&e1, &e2, &e3, &e4, &e5, &e6, &e7, &e8};
465 SECTION("Filter with events part of initial maximal set")
467 EventSet interesting_bunch{&e2, &e4, &e7, &e8};
469 maximal_subsets_iterator first(
470 C, [&interesting_bunch](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
471 maximal_subsets_iterator last;
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()]++;
482 // The empty set should (still) appear only once
483 REQUIRE(maximal_subset_counts[0] == 1);
485 // 4 is the number of nodes in the `interesting_bunch`
486 REQUIRE(maximal_subset_counts[1] == 4);
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);
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);
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);
499 SECTION("Filter with interesting subset not initially part of the maximal set")
501 EventSet interesting_bunch{&e3, &e5, &e6};
503 maximal_subsets_iterator first(
504 C, [&interesting_bunch](const UnfoldingEvent* e) { return interesting_bunch.contains(e); });
505 maximal_subsets_iterator last;
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()]++;
516 // The empty set should (still) appear only once
517 REQUIRE(maximal_subset_counts[0] == 1);
519 // 3 is the number of nodes in the `interesting_bunch`
520 REQUIRE(maximal_subset_counts[1] == 3);
522 // 2 = e3, e5 and e3, e6
523 REQUIRE(maximal_subset_counts[2] == 2);
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);
532 TEST_CASE("simgrid::mc::udpor::maximal_subsets_iterator: Stress Test for Maximal Subsets Iteration")
534 // The following tests concern the given event structure:
539 // +------* e4 *e5 e6 e7
543 // | e11 e12 e13 e14 e15
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};
566 SECTION("Every subset iterated over is maximal")
568 maximal_subsets_iterator first(C);
569 maximal_subsets_iterator last;
571 // Make sure we actually have something to iterate over
572 REQUIRE(first != last);
574 for (; first != last; ++first) {
575 REQUIRE((*first).size() <= C.get_events().size());
576 REQUIRE((*first).is_maximal());
580 SECTION("Test that the maximal set ordering is equivalent to that of the configuration's events")
582 maximal_subsets_iterator first_config(C);
583 maximal_subsets_iterator first_events(C.get_events());
584 maximal_subsets_iterator last;
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);
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;
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);
602 // Iteration with events directly should now also be finished
603 REQUIRE(first_events == last);
607 TEST_CASE("simgrid::mc::udpor::Configuration: Latest Transitions")
609 // The following tests concern the given event structure (labeled as "event(actor)")
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);
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);
635 SECTION("Test that the latest events are correct on initialization")
637 SECTION("Empty configuration has no events")
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());
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());
649 SECTION("Missing two actors")
651 Configuration C{&e1};
652 REQUIRE(C.get_latest_event_of(1).has_value());
653 REQUIRE(C.get_latest_event_of(1).value() == &e1);
655 REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
656 REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
658 REQUIRE(C.get_latest_action_of(1).has_value());
659 REQUIRE(C.get_latest_action_of(1).value() == t1.get());
661 REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
662 REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
665 SECTION("Two events with one actor yields the latest event")
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);
671 REQUIRE_FALSE(C.get_latest_event_of(2).has_value());
672 REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
674 REQUIRE(C.get_latest_action_of(1).has_value());
675 REQUIRE(C.get_latest_action_of(1).value() == t2.get());
677 REQUIRE_FALSE(C.get_latest_action_of(2).has_value());
678 REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
681 SECTION("Two events with two actors")
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);
687 REQUIRE(C.get_latest_event_of(2).has_value());
688 REQUIRE(C.get_latest_event_of(2).value() == &e3);
690 REQUIRE_FALSE(C.get_latest_event_of(3).has_value());
692 REQUIRE(C.get_latest_action_of(1).has_value());
693 REQUIRE(C.get_latest_action_of(1).value() == t1.get());
695 REQUIRE(C.get_latest_action_of(2).has_value());
696 REQUIRE(C.get_latest_action_of(2).value() == t3.get());
698 REQUIRE_FALSE(C.get_latest_action_of(3).has_value());
701 SECTION("Three different actors actors")
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);
707 REQUIRE(C.get_latest_event_of(2).has_value());
708 REQUIRE(C.get_latest_event_of(2).value() == &e5);
710 REQUIRE(C.get_latest_event_of(3).has_value());
711 REQUIRE(C.get_latest_event_of(3).value() == &e4);
713 REQUIRE(C.get_latest_action_of(1).has_value());
714 REQUIRE(C.get_latest_action_of(1).value() == t2.get());
716 REQUIRE(C.get_latest_action_of(2).has_value());
717 REQUIRE(C.get_latest_action_of(2).value() == t5.get());
719 REQUIRE(C.get_latest_action_of(3).has_value());
720 REQUIRE(C.get_latest_action_of(3).value() == t4.get());
724 SECTION("Test that the latest events are correct when adding new events")
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());
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());
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());
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());
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());
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());
796 TEST_CASE("simgrid::mc::udpor::Configuration: Computing Full Alternatives in Reader/Writer Example")
798 // The following tests concern the given event structure that is given as
799 // an example in figure 1 of the original UDPOR paper.
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`
815 auto e0 = std::make_unique<UnfoldingEvent>(
816 EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
817 const auto* e0_handle = e0.get();
819 auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}),
820 std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
821 const auto* e1_handle = e1.get();
823 auto e2 = std::make_unique<UnfoldingEvent>(
824 EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
825 const auto* e2_handle = e2.get();
827 auto e3 = std::make_unique<UnfoldingEvent>(
828 EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
829 const auto* e3_handle = e3.get();
831 auto e4 = std::make_unique<UnfoldingEvent>(
832 EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
833 const auto* e4_handle = e4.get();
835 auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}),
836 std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
837 const auto* e5_handle = e5.get();
839 auto e6 = std::make_unique<UnfoldingEvent>(
840 EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
841 const auto* e6_handle = e6.get();
843 auto e7 = std::make_unique<UnfoldingEvent>(
844 EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
845 const auto* e7_handle = e7.get();
847 auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}),
848 std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
849 const auto* e8_handle = e8.get();
851 auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}),
852 std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
853 const auto* e9_handle = e9.get();
855 auto e10 = std::make_unique<UnfoldingEvent>(
856 EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
857 const auto* e10_handle = e10.get();
859 SECTION("Alternative computation call 1")
861 // During the first call to Alt(C, D + {e}),
862 // UDPOR believes `U` to be the following:
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])
875 // Thus the computation is (since D is empty at first)
877 // Alt(C, D + {e}) --> Alt({e0, e1, e2}, {e3})
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};
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));
893 const auto alternative = C.compute_alternative_to(D_plus_e, U);
894 REQUIRE_FALSE(alternative.has_value());
897 SECTION("Alternative computation call 2")
899 // During the second call to Alt(C, D + {e}),
900 // UDPOR believes `U` to be the following:
909 // C := {e0, e1} and `Explore(C, D, A)` picked `e2`.
911 // Thus the computation is (since D is still empty)
913 // Alt(C, D + {e}) --> Alt({e0, e1}, {e2})
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};
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));
930 const auto alternative = C.compute_alternative_to(D_plus_e, U);
931 REQUIRE_FALSE(alternative.has_value());
934 SECTION("Alternative computation call 3")
936 // During the thrid call to Alt(C, D + {e}),
937 // UDPOR believes `U` to be the following:
946 // C := {e0} and `Explore(C, D, A)` picked `e1`.
948 // Thus the computation is (since D is still empty)
950 // Alt(C, D + {e}) --> Alt({e0}, {e1})
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};
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));
966 const auto alternative = C.compute_alternative_to(D_plus_e, U);
967 REQUIRE(alternative.has_value());
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}) ||
973 alternative.value().get_events() == EventSet({e0_handle, e7_handle})));
976 SECTION("Alternative computation call 4")
978 // During the fourth call to Alt(C, D + {e}),
979 // UDPOR believes `U` to be the following:
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])
993 // Thus the computation is (since D is {e1})
995 // Alt(C, D + {e}) --> Alt({e0, e4, e5}, {e1, e6})
997 // where U is given above. There are no alternatives in this
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};
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));
1015 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1016 REQUIRE_FALSE(alternative.has_value());
1019 SECTION("Alternative computation call 5")
1021 // During the fifth call to Alt(C, D + {e}),
1022 // UDPOR believes `U` to be the following:
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])
1036 // Thus the computation is (since D is {e1})
1038 // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5})
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}.
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};
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);
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}) ||
1063 alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle}) ||
1064 alternative.value().get_events() == EventSet({e0_handle, e4_handle, e7_handle, e8_handle})));
1067 SECTION("Alternative computation call 6")
1069 // During the sixth call to Alt(C, D + {e}),
1070 // UDPOR believes `U` to be the following:
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])
1084 // Thus the computation is (since D is {e1, e5} [see the last step])
1086 // Alt(C, D + {e}) --> Alt({e0, e4, e7}, {e1, e5, e8})
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};
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));
1105 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1106 REQUIRE_FALSE(alternative.has_value());
1109 SECTION("Alternative computation call 7")
1111 // During the seventh call to Alt(C, D + {e}),
1112 // UDPOR believes `U` to be the following:
1122 // C := {e0, e4} and `Explore(C, D, A)` picked `e7`
1124 // Thus the computation is (since D is {e1, e5} [see call 5])
1126 // Alt(C, D + {e}) --> Alt({e0, e4}, {e1, e5, e7})
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};
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));
1145 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1146 REQUIRE_FALSE(alternative.has_value());
1149 SECTION("Alternative computation call 8")
1151 // During the eigth call to Alt(C, D + {e}),
1152 // UDPOR believes `U` to be the following:
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.
1166 // Thus the computation is (since D = {e1})
1168 // Alt(C, D + {e}) --> Alt({e0}, {e1, e4})
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
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};
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));
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}));
1199 SECTION("Alternative computation call 9")
1201 // During the ninth call to Alt(C, D + {e}),
1202 // UDPOR believes `U` to be the following:
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]).
1216 // Thus the computation is (since D = {e1, e4} [see the previous step])
1218 // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e10})
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};
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));
1236 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1237 REQUIRE_FALSE(alternative.has_value());
1240 SECTION("Alternative computation call 10")
1242 // During the tenth call to Alt(C, D + {e}),
1243 // UDPOR believes `U` to be the following:
1253 // C := {e0, e7} and `Explore(C, D, A)` picked `e9`.
1255 // Thus the computation is (since D = {e1, e4} [see call 8])
1257 // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e9})
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};
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));
1275 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1276 REQUIRE_FALSE(alternative.has_value());
1279 SECTION("Alternative computation call 11 (final call)")
1281 // During the eleventh and final call to Alt(C, D + {e}),
1282 // UDPOR believes `U` to be the following:
1292 // C := {e0} and `Explore(C, D, A)` picked `e7`.
1294 // Thus the computation is (since D = {e1, e4} [see call 8])
1296 // Alt(C, D + {e}) --> Alt({e0}, {e1, e4, e7})
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};
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));
1315 const auto alternative = C.compute_alternative_to(D_plus_e, U);
1316 REQUIRE_FALSE(alternative.has_value());
1319 SECTION("Alternative computation next")
1321 SECTION("Followed {e0, e7} first")
1323 const EventSet D{e1_handle, e7_handle};
1324 const Configuration C{e0_handle};
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));
1338 const auto alternative = C.compute_alternative_to(D, U);
1339 REQUIRE(alternative.has_value());
1341 // In this case, only {e0, e4} is a valid alternative
1342 REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e4_handle, e5_handle}));
1345 SECTION("Followed {e0, e4} first")
1347 const EventSet D{e1_handle, e4_handle};
1348 const Configuration C{e0_handle};
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));
1362 const auto alternative = C.compute_alternative_to(D, U);
1363 REQUIRE(alternative.has_value());
1365 // In this case, only {e0, e7} is a valid alternative
1366 REQUIRE(alternative.value().get_events() == EventSet({e0_handle, e7_handle, e9_handle}));