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/EventSet.hpp"
8 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
10 using namespace simgrid::mc::udpor;
12 TEST_CASE("simgrid::mc::udpor::EventSet: Initial conditions when creating sets")
14 SECTION("Initialization with no elements")
16 SECTION("Default initializer")
19 REQUIRE(event_set.size() == 0);
20 REQUIRE(event_set.empty());
23 SECTION("Set initializer")
25 EventSet event_set({});
26 REQUIRE(event_set.size() == 0);
27 REQUIRE(event_set.empty());
30 SECTION("List initialization")
33 REQUIRE(event_set.size() == 0);
34 REQUIRE(event_set.empty());
38 SECTION("Initialization with one or more elements")
40 UnfoldingEvent e1, e2, e3;
42 SECTION("Set initializer")
44 EventSet event_set({&e1, &e2, &e3});
45 REQUIRE(event_set.size() == 3);
46 REQUIRE(event_set.contains(&e1));
47 REQUIRE(event_set.contains(&e2));
48 REQUIRE(event_set.contains(&e3));
49 REQUIRE_FALSE(event_set.empty());
52 SECTION("List initialization")
54 UnfoldingEvent e1, e2, e3;
55 EventSet event_set{&e1, &e2, &e3};
56 REQUIRE(event_set.size() == 3);
57 REQUIRE(event_set.contains(&e1));
58 REQUIRE(event_set.contains(&e2));
59 REQUIRE(event_set.contains(&e3));
60 REQUIRE_FALSE(event_set.empty());
65 TEST_CASE("simgrid::mc::udpor::EventSet: Insertions")
68 UnfoldingEvent e1, e2, e3;
70 SECTION("Inserting unique elements")
72 event_set.insert(&e1);
73 REQUIRE(event_set.size() == 1);
74 REQUIRE(event_set.contains(&e1));
75 REQUIRE_FALSE(event_set.empty());
77 event_set.insert(&e2);
78 REQUIRE(event_set.size() == 2);
79 REQUIRE(event_set.contains(&e2));
80 REQUIRE_FALSE(event_set.empty());
82 SECTION("Check contains inserted elements")
84 REQUIRE(event_set.contains(&e1));
85 REQUIRE(event_set.contains(&e2));
86 REQUIRE_FALSE(event_set.contains(&e3));
90 SECTION("Inserting duplicate elements")
92 event_set.insert(&e1);
93 REQUIRE(event_set.size() == 1);
94 REQUIRE(event_set.contains(&e1));
95 REQUIRE_FALSE(event_set.empty());
97 event_set.insert(&e1);
98 REQUIRE(event_set.size() == 1);
99 REQUIRE(event_set.contains(&e1));
100 REQUIRE_FALSE(event_set.empty());
102 SECTION("Check contains inserted elements")
104 REQUIRE(event_set.contains(&e1));
105 REQUIRE_FALSE(event_set.contains(&e2));
106 REQUIRE_FALSE(event_set.contains(&e3));
111 TEST_CASE("simgrid::mc::udpor::EventSet: Deletions")
113 UnfoldingEvent e1, e2, e3, e4;
114 EventSet event_set({&e1, &e2, &e3});
116 SECTION("Remove an element already present")
118 REQUIRE(event_set.contains(&e1));
120 // event_set = {e2, e3}
121 event_set.remove(&e1);
124 // 1. the size decreases by exactly 1
125 // 2. the set remains unempty
126 // 3. the other elements are still contained in the set
127 REQUIRE(event_set.size() == 2);
128 REQUIRE_FALSE(event_set.contains(&e1));
129 REQUIRE(event_set.contains(&e2));
130 REQUIRE(event_set.contains(&e3));
131 REQUIRE_FALSE(event_set.empty());
133 SECTION("Remove a single element more than once")
135 // event_set = {e2, e3}
136 event_set.remove(&e1);
137 REQUIRE(event_set.size() == 2);
138 REQUIRE_FALSE(event_set.contains(&e1));
139 REQUIRE(event_set.contains(&e2));
140 REQUIRE(event_set.contains(&e3));
141 REQUIRE_FALSE(event_set.empty());
144 SECTION("Remove more than one element")
147 event_set.remove(&e2);
149 REQUIRE(event_set.size() == 1);
150 REQUIRE_FALSE(event_set.contains(&e1));
151 REQUIRE_FALSE(event_set.contains(&e2));
152 REQUIRE(event_set.contains(&e3));
153 REQUIRE_FALSE(event_set.empty());
156 event_set.remove(&e3);
158 REQUIRE(event_set.size() == 0);
159 REQUIRE_FALSE(event_set.contains(&e1));
160 REQUIRE_FALSE(event_set.contains(&e2));
161 REQUIRE_FALSE(event_set.contains(&e3));
162 REQUIRE(event_set.empty());
166 SECTION("Remove an element absent from the set")
168 REQUIRE_FALSE(event_set.contains(&e4));
170 // event_set = {e1, e2, e3}
171 event_set.remove(&e4);
172 REQUIRE(event_set.size() == 3);
173 REQUIRE(event_set.contains(&e1));
174 REQUIRE(event_set.contains(&e2));
175 REQUIRE(event_set.contains(&e3));
177 // Ensure e4 isn't somehow added
178 REQUIRE_FALSE(event_set.contains(&e4));
179 REQUIRE_FALSE(event_set.empty());
183 TEST_CASE("simgrid::mc::udpor::EventSet: Set Equality")
185 UnfoldingEvent e1, e2, e3, e4;
186 EventSet A{&e1, &e2, &e3}, B{&e1, &e2, &e3}, C{&e1, &e2, &e3};
188 SECTION("Equality implies containment")
192 for (const auto& e : A) {
193 REQUIRE(B.contains(e));
196 for (const auto& e : B) {
197 REQUIRE(A.contains(e));
201 SECTION("Containment implies equality")
203 for (const auto& e : A) {
204 REQUIRE(B.contains(e));
207 for (const auto& e : C) {
208 REQUIRE(C.contains(e));
214 SECTION("Equality is an equivalence relation")
235 SECTION("Equality after copy (assignment + constructor)")
240 REQUIRE(A == A_copy);
241 REQUIRE(A == A_copy2);
244 SECTION("Equality after move constructor")
247 EventSet A_move(std::move(A));
248 REQUIRE(A_move == A_copy);
251 SECTION("Equality after move-assignment")
254 EventSet A_move = std::move(A);
255 REQUIRE(A_move == A_copy);
259 TEST_CASE("simgrid::mc::udpor::EventSet: Set Union Tests")
261 UnfoldingEvent e1, e2, e3, e4;
264 EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3};
266 SECTION("Unions with no effect")
270 SECTION("Self union")
273 EventSet A_union = A.make_union(A);
274 REQUIRE(A == A_copy);
277 REQUIRE(A == A_copy);
280 SECTION("Union with empty set")
282 // A = A union empty set
283 EventSet A_union = A.make_union(EventSet());
284 REQUIRE(A == A_union);
286 A.form_union(EventSet());
287 REQUIRE(A == A_copy);
290 SECTION("Union with an equivalent set")
292 // A = A union B if B == A
293 EventSet A_equiv{&e1, &e2, &e3};
294 REQUIRE(A == A_equiv);
296 EventSet A_union = A.make_union(A_equiv);
297 REQUIRE(A_union == A_copy);
299 A.form_union(A_equiv);
300 REQUIRE(A == A_copy);
303 SECTION("Union with a subset")
305 // A = A union D if D is a subset of A
306 EventSet A_union = A.make_union(D);
307 REQUIRE(A == A_union);
310 REQUIRE(A == A_copy);
314 SECTION("Unions with partial overlaps")
316 EventSet A_union_B = A.make_union(B);
317 REQUIRE(A_union_B == C);
322 EventSet B_union_D = B.make_union(D);
323 REQUIRE(B_union_D == C);
329 SECTION("Set union properties")
331 SECTION("Union operator is symmetric")
333 EventSet A_union_B = A.make_union(B);
334 EventSet B_union_A = B.make_union(A);
335 REQUIRE(A_union_B == B_union_A);
338 SECTION("Union operator commutes")
340 // The last SECTION tested pair-wise
341 // equivalence, so we only check
343 EventSet AD = A.make_union(D);
344 EventSet AC = A.make_union(C);
345 EventSet CD = D.make_union(C);
347 EventSet ADC = AD.make_union(C);
348 EventSet ACD = AC.make_union(D);
349 EventSet CDA = CD.make_union(A);
354 // Test `form_union()` in the same way
360 A.form_union(C_copy);
361 A.form_union(D_copy);
363 D.form_union(A_copy);
364 D.form_union(C_copy);
376 TEST_CASE("simgrid::mc::udpor::EventSet: Set Difference Tests")
378 UnfoldingEvent e1, e2, e3, e4;
381 // A is a subset of C
382 // B is a subset of C
383 // D is a subset of A and C
384 // E is a subset of B and C
385 // F is a subset of A, C, and D
386 EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e4}, F{&e1};
388 SECTION("Difference with no effect")
390 SECTION("Difference with empty set")
392 EventSet A_copy = A.subtracting(EventSet());
393 REQUIRE(A == A_copy);
395 A.subtract(EventSet());
396 REQUIRE(A == A_copy);
399 SECTION("Difference with empty intersection")
401 // A intersection E = empty set
402 EventSet A_copy = A.subtracting(E);
403 REQUIRE(A == A_copy);
406 REQUIRE(A == A_copy);
408 EventSet D_copy = D.subtracting(E);
409 REQUIRE(D == D_copy);
412 REQUIRE(D == D_copy);
416 SECTION("Difference with some overlap")
419 EventSet A_minus_B = A.subtracting(B);
420 REQUIRE(A_minus_B == F);
422 // B - D = {&e2, &e4}
423 EventSet B_minus_D = B.subtracting(D);
424 REQUIRE(B_minus_D == EventSet({&e2, &e4}));
427 SECTION("Difference with complete overlap")
429 SECTION("Difference with same set gives empty set")
431 REQUIRE(A.subtracting(A) == EventSet());
432 REQUIRE(B.subtracting(B) == EventSet());
433 REQUIRE(C.subtracting(C) == EventSet());
434 REQUIRE(D.subtracting(D) == EventSet());
435 REQUIRE(E.subtracting(E) == EventSet());
436 REQUIRE(F.subtracting(F) == EventSet());
439 SECTION("Difference with superset gives empty set")
441 REQUIRE(A.subtracting(C) == EventSet());
442 REQUIRE(B.subtracting(C) == EventSet());
443 REQUIRE(D.subtracting(A) == EventSet());
444 REQUIRE(D.subtracting(C) == EventSet());
445 REQUIRE(E.subtracting(B) == EventSet());
446 REQUIRE(E.subtracting(C) == EventSet());
447 REQUIRE(F.subtracting(A) == EventSet());
448 REQUIRE(F.subtracting(C) == EventSet());
449 REQUIRE(F.subtracting(D) == EventSet());
454 TEST_CASE("simgrid::mc::udpor::EventSet: Subset Tests")
456 UnfoldingEvent e1, e2, e3, e4;
458 // A is a subset of C only
459 // B is a subset of C only
460 // D is a subset of C and A
461 // D is NOT a subset of B
462 // B is NOT a subset of D
464 EventSet A{&e1, &e2, &e3}, B{&e2, &e3, &e4}, C{&e1, &e2, &e3, &e4}, D{&e1, &e3}, E{&e2, &e3}, F{&e1, &e2, &e3};
466 SECTION("Subset operator properties")
468 SECTION("Subset operator is not commutative")
470 REQUIRE(A.is_subset_of(C));
471 REQUIRE_FALSE(C.is_subset_of(A));
473 SECTION("Commutativity implies equality and vice versa")
475 REQUIRE(A.is_subset_of(F));
476 REQUIRE(F.is_subset_of(A));
480 REQUIRE(A.is_subset_of(F));
481 REQUIRE(F.is_subset_of(A));
485 SECTION("Subset operator is transitive")
487 REQUIRE(D.is_subset_of(A));
488 REQUIRE(A.is_subset_of(C));
489 REQUIRE(D.is_subset_of(C));
490 REQUIRE(E.is_subset_of(B));
491 REQUIRE(B.is_subset_of(C));
492 REQUIRE(E.is_subset_of(C));
495 SECTION("Subset operator is reflexive")
497 REQUIRE(A.is_subset_of(A));
498 REQUIRE(B.is_subset_of(B));
499 REQUIRE(C.is_subset_of(C));
500 REQUIRE(D.is_subset_of(D));
501 REQUIRE(E.is_subset_of(E));
502 REQUIRE(F.is_subset_of(F));