src/mc/explo/odpor/Execution_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/odpor/Execution.hpp"
   8 #include "src/mc/explo/udpor/udpor_tests_private.hpp"
   9 #include "src/mc/transition/TransitionComm.hpp"
  10
  11 using namespace simgrid::mc;
  12 using namespace simgrid::mc::odpor;
  13 using namespace simgrid::mc::udpor;
  14
  15 TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
  16 {
  17   Execution execution;
  18   REQUIRE(execution.empty());
  19   REQUIRE(execution.size() == 0);
  20   REQUIRE_FALSE(execution.get_latest_event_handle().has_value());
  21 }
  22
  23 TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
  24 {
  25   SECTION("Example 1")
  26   {
  27     // We check each permutation for happens before
  28     // among the given actions added to the execution
  29     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
  30     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
  31     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  32     const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
  33
  34     Execution execution;
  35     execution.push_transition(a1);
  36     execution.push_transition(a2);
  37     execution.push_transition(a3);
  38     execution.push_transition(a4);
  39
  40     SECTION("Happens-before is irreflexive")
  41     {
  42       REQUIRE_FALSE(execution.happens_before(0, 0));
  43       REQUIRE_FALSE(execution.happens_before(1, 1));
  44       REQUIRE_FALSE(execution.happens_before(2, 2));
  45       REQUIRE_FALSE(execution.happens_before(3, 3));
  46     }
  47
  48     SECTION("Happens-before values for each pair of events")
  49     {
  50       REQUIRE_FALSE(execution.happens_before(0, 1));
  51       REQUIRE_FALSE(execution.happens_before(0, 2));
  52       REQUIRE(execution.happens_before(0, 3));
  53       REQUIRE_FALSE(execution.happens_before(1, 2));
  54       REQUIRE_FALSE(execution.happens_before(1, 3));
  55       REQUIRE_FALSE(execution.happens_before(2, 3));
  56     }
  57
  58     SECTION("Happens-before is a subset of 'occurs-before' ")
  59     {
  60       REQUIRE_FALSE(execution.happens_before(1, 0));
  61       REQUIRE_FALSE(execution.happens_before(2, 0));
  62       REQUIRE_FALSE(execution.happens_before(3, 0));
  63       REQUIRE_FALSE(execution.happens_before(2, 1));
  64       REQUIRE_FALSE(execution.happens_before(3, 1));
  65       REQUIRE_FALSE(execution.happens_before(3, 2));
  66     }
  67   }
  68
  69   SECTION("Example 2")
  70   {
  71     const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
  72     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  73     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  74     const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  75
  76     // Notice that `a5` and `a6` are executed by the same actor; thus, although
  77     // the actor is executing independent actions, each still "happen-before"
  78     // the another
  79
  80     Execution execution;
  81     execution.push_transition(a1);
  82     execution.push_transition(a2);
  83     execution.push_transition(a3);
  84     execution.push_transition(a4);
  85
  86     SECTION("Happens-before is irreflexive")
  87     {
  88       REQUIRE_FALSE(execution.happens_before(0, 0));
  89       REQUIRE_FALSE(execution.happens_before(1, 1));
  90       REQUIRE_FALSE(execution.happens_before(2, 2));
  91       REQUIRE_FALSE(execution.happens_before(3, 3));
  92     }
  93
  94     SECTION("Happens-before values for each pair of events")
  95     {
  96       REQUIRE_FALSE(execution.happens_before(0, 1));
  97       REQUIRE_FALSE(execution.happens_before(0, 2));
  98       REQUIRE_FALSE(execution.happens_before(0, 3));
  99       REQUIRE(execution.happens_before(1, 2));
 100       REQUIRE(execution.happens_before(1, 3));
 101       REQUIRE(execution.happens_before(2, 3));
 102     }
 103
 104     SECTION("Happens-before is a subset of 'occurs-before'")
 105     {
 106       REQUIRE_FALSE(execution.happens_before(1, 0));
 107       REQUIRE_FALSE(execution.happens_before(2, 0));
 108       REQUIRE_FALSE(execution.happens_before(3, 0));
 109       REQUIRE_FALSE(execution.happens_before(2, 1));
 110       REQUIRE_FALSE(execution.happens_before(3, 1));
 111       REQUIRE_FALSE(execution.happens_before(3, 2));
 112     }
 113   }
 114
 115   SECTION("Example 3: Happens-before is transitively-closed")
 116   {
 117     // Given a reversible race between events `e1` and `e3` in a simulation,
 118     // we assert that `e5` would be eliminated from being contained in
 119     // the sequence `notdep(e1, E)`
 120     const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 121     const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 122     const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 123     const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 124     const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 125
 126     Execution execution;
 127     execution.push_transition(e0);
 128     execution.push_transition(e1);
 129     execution.push_transition(e2);
 130     execution.push_transition(e3);
 131     execution.push_transition(e4);
 132
 133     REQUIRE(execution.happens_before(0, 2));
 134     REQUIRE(execution.happens_before(2, 4));
 135     REQUIRE(execution.happens_before(0, 4));
 136   }
 137 }
 138
 139 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
 140 {
 141   SECTION("Example 1")
 142   {
 143     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 144     const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 145     const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 146     const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 147     const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 148
 149     Execution execution;
 150     execution.push_transition(a1);
 151     execution.push_transition(a2);
 152     execution.push_transition(a3);
 153     execution.push_transition(a4);
 154     execution.push_transition(a5);
 155
 156     // Nothing comes before event 0
 157     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 158
 159     // Events 0 and 1 are independent
 160     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 161
 162     // 2 and 1 are executed by different actors and happen right after each other
 163     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
 164
 165     // Although a3 and a4 are dependent, they are executed by the same actor
 166     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
 167
 168     // Event 4 is in a race with neither event 0 nor event 2 since those events
 169     // "happen-before" event 3 with which event 4 races
 170     //
 171     // Furthermore, event 1 is run by the same actor and thus also is not in a race.
 172     // Hence, only event 3 races with event 4
 173     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
 174   }
 175
 176   SECTION("Example 2: Events with multiple races")
 177   {
 178     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 179     const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 180     const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 181     const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 182
 183     Execution execution;
 184     execution.push_transition(a1);
 185     execution.push_transition(a2);
 186     execution.push_transition(a3);
 187     execution.push_transition(a4);
 188
 189     // Nothing comes before event 0
 190     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 191
 192     // Events 0 and 1 are independent
 193     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 194
 195     // Event 2 is independent with event 1 and run by the same actor as event 0
 196     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
 197
 198     // All events are dependent with event 3, but event 0 "happens-before" event 2
 199     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
 200
 201     SECTION("Check initials with respect to event 1")
 202     {
 203       // First, note that v := notdep(1, execution).p == {e2}.{e3} == {e2, e3}
 204       // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
 205       // with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
 206       // so it is an initial of E' wrt. `v`
 207       const auto initial_wrt_event1 = execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{});
 208       REQUIRE(initial_wrt_event1 == std::unordered_set<aid_t>{1});
 209     }
 210
 211     SECTION("Check initials with respect to event 2")
 212     {
 213       // First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
 214       // e3 has nothing happening before it in dom_E(v), so it is an initial
 215       // of E' wrt. `v`
 216       const auto initial_wrt_event2 = execution.get_missing_source_set_actors_from(2, std::unordered_set<aid_t>{});
 217       REQUIRE(initial_wrt_event2 == std::unordered_set<aid_t>{3});
 218     }
 219   }
 220
 221   SECTION("Example 3: Testing 'Lock' Example")
 222   {
 223     // In this example, `e0` and `e1` are lock actions that
 224     // are in a race. We assert that
 225     const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 226     const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 227     const auto e2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 228     const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 229     const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 230
 231     Execution execution;
 232     execution.push_transition(e0);
 233     execution.push_transition(e1);
 234     execution.push_transition(e2);
 235     execution.push_transition(e3);
 236     execution.push_transition(e4);
 237     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
 238   }
 239
 240   SECTION("Example 4: Indirect Races")
 241   {
 242     const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 243     const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 244     const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 245     const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 246     const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
 247     const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 248     const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 249     const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 250     const auto a8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 251     const auto a9 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 252
 253     Execution execution;
 254     execution.push_transition(a0);
 255     execution.push_transition(a1);
 256     execution.push_transition(a2);
 257     execution.push_transition(a3);
 258     execution.push_transition(a4);
 259     execution.push_transition(a5);
 260     execution.push_transition(a6);
 261     execution.push_transition(a7);
 262     execution.push_transition(a8);
 263     execution.push_transition(a9);
 264
 265     // Nothing comes before event 0
 266     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 267
 268     // Events 0 and 1 are independent
 269     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 270
 271     // Events 1 and 2 are independent
 272     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
 273
 274     // Events 1 and 3 are independent; the rest are executed by the same actor
 275     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
 276
 277     // 1. Events 3 and 4 race
 278     // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4
 279     // 3. Events 1 and 4 do NOT race since 1 is independent of 4
 280     // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4
 281     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
 282
 283     // Events 4 and 5 race; and because everyone before 4 (including 3) either
 284     // a) happens-before, b) races, or c) does not race with 4, 4 is the race
 285     REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{4});
 286
 287     // The same logic that applied to event 5 applies to event 6
 288     REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
 289
 290     // The same logic applies, except that this time since events 6 and 7 are run
 291     // by the same actor, they don'tt actually race with one another
 292     REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{});
 293
 294     // Event 8 is independent with everything
 295     REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
 296
 297     // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9.
 298     // The same logic above eliminates events before 6
 299     REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});
 300   }
 301 }
 302
 303 TEST_CASE("simgrid::mc::odpor::Execution: notdep(e, E) Simulation")
 304 {
 305   // Given a reversible race between events `e1` and `e3` in a simulation,
 306   // we assert that `e5` would be eliminated from being contained in
 307   // the sequence `notdep(e1, E)`
 308   const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 309   const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 310   const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 311   const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 312   const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 313
 314   Execution execution;
 315   execution.push_transition(e0);
 316   execution.push_transition(e1);
 317   execution.push_transition(e2);
 318   execution.push_transition(e3);
 319   execution.push_transition(e4);
 320
 321   REQUIRE(execution.happens_before(0, 4));
 322 }
 323
 324 TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
 325 {
 326   SECTION("Complete independence")
 327   {
 328     // Every transition is independent with every other and run by different actors. Hopefully
 329     // we say that the events are independent with each other...
 330     const auto a0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 331     const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 332     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
 333     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 334     const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 5);
 335     const auto a5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 6);
 336     const auto a6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
 337     const auto a7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
 338     Execution execution;
 339     execution.push_transition(a0);
 340     execution.push_transition(a1);
 341     execution.push_transition(a2);
 342     execution.push_transition(a3);
 343
 344     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6));
 345     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a5}, a1));
 346     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a1}, a0));
 347     REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a7, a7, a1}, a3));
 348     REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a4, a0, a1}, a3));
 349     REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a0, a7, a1}, a2));
 350
 351     // In this case, we notice that `a6` and `a7` are executed by the same actor.
 352     // Hence, a6 cannot be independent with extending the execution with a4.a5.a7.
 353     // Notice that we are treating *a6* as the next step of actor 7 (that is what we
 354     // supplied as an argument)
 355     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6));
 356   }
 357
 358   SECTION("Independence is trivial with an empty extension")
 359   {
 360     REQUIRE(Execution().is_independent_with_execution_of(
 361         PartialExecution{}, std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1)));
 362   }
 363
 364   SECTION("Dependencies stopping independence from being possible")
 365   {
 366     const auto a0    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 367     const auto a1    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 368     const auto a2    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 369     const auto a3    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 370     const auto a4    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 371     const auto a5    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 372     const auto a6    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 373     const auto a7    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 374     const auto a8    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 375     const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 376     Execution execution;
 377     execution.push_transition(a0);
 378     execution.push_transition(a1);
 379     execution.push_transition(a2);
 380     execution.push_transition(a3);
 381
 382     // We see that although `a4` comes after `a1` with which it is dependent, it
 383     // would come before "a6" in the partial execution `w`, so it would not be independent
 384     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4));
 385
 386     // Removing `a6` from the picture, though, gives us the independence we're looking for.
 387     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4));
 388
 389     // BUT, we we ask about a transition which is run by the same actor, even if they would be
 390     // independent otherwise, we again lose independence
 391     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4));
 392
 393     // This is a more interesting case:
 394     // `indep` clearly is independent with the rest of the series, even though
 395     // there are dependencies among the other events in the partial execution
 396     REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep));
 397
 398     // This ensures that independence is trivial with an empty partial execution
 399     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{}, a1));
 400   }
 401 }
 402
 403 TEST_CASE("simgrid::mc::odpor::Execution: Initials Test")
 404 {
 405   const auto a0    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 406   const auto a1    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 407   const auto a2    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 408   const auto a3    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 409   const auto a4    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 410   const auto a5    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 411   const auto a6    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 412   const auto a7    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 413   const auto a8    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 414   const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 415   Execution execution;
 416   execution.push_transition(a0);
 417   execution.push_transition(a1);
 418   execution.push_transition(a2);
 419   execution.push_transition(a3);
 420
 421   SECTION("Initials trivial with empty executions")
 422   {
 423     // There are no initials for an empty extension since
 424     // a requirement is that the actor be contained in the
 425     // extension itself
 426     REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 0));
 427     REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 1));
 428     REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 2));
 429     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 0));
 430     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 1));
 431     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 2));
 432   }
 433
 434   SECTION("The first actor is always an initial")
 435   {
 436     // Even in the case that the action is dependent with every
 437     // other, if it is the first action to occur as part of the
 438     // extension of the execution sequence, by definition it is
 439     // an initial (recall that initials intuitively tell you which
 440     // actions can be run starting from an execution `E`; if we claim
 441     // to witness `E.w`, then clearly at least the first step of `w` is an initial)
 442     REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a3}, a3->aid_));
 443     REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a2, a3, a6}, a2->aid_));
 444     REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a6, a1, a0}, a6->aid_));
 445     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a0, a1, a2, a3}, a0->aid_));
 446     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a5, a2, a8, a7, a6, a0}, a5->aid_));
 447     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a8, a7, a1}, a8->aid_));
 448   }
 449
 450   SECTION("Example: Disqualified and re-qualified after switching ordering")
 451   {
 452     // Even though actor `2` executes an independent
 453     // transition later on, it is blocked since its first transition
 454     // is dependent with actor 1's transition
 455     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a5, indep}, 2));
 456
 457     // However, if actor 2 executes its independent action first, it DOES become an initial
 458     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, indep, a5}, 2));
 459   }
 460
 461   SECTION("Example: Large partial executions")
 462   {
 463     // The record trace is `1 3 4 4 3 1 4 2`
 464
 465     // Actor 1 starts the execution
 466     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 1));
 467
 468     // Actor 2 all the way at the end is independent with everybody: despite
 469     // the tangle that comes before it, we can more it to the front with no issue
 470     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 2));
 471
 472     // Actor 3 is eliminated since `a1` is dependent with `a2`
 473     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 3));
 474
 475     // Likewise with actor 4
 476     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 4));
 477   }
 478 }
 479
 480 TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
 481 {
 482   const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 483   const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 484   const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 485   const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 486   const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 487   const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 488
 489   Execution execution;
 490   execution.push_transition(a0);
 491   execution.push_transition(a1);
 492   execution.push_transition(a2);
 493   execution.push_transition(a3);
 494   execution.push_transition(a4);
 495   execution.push_transition(a5);
 496
 497   SECTION("Equivalent insertions")
 498   {
 499     SECTION("Example: Eliminated through independence")
 500     {
 501       // TODO: Is this even a sensible question to ask if the two sequences
 502       // don't agree upon what each actor executed after `E`?
 503       const auto insertion =
 504           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
 505       REQUIRE(insertion.has_value());
 506       REQUIRE(insertion.value() == PartialExecution{});
 507     }
 508
 509     SECTION("Exact match yields empty set")
 510     {
 511       const auto insertion =
 512           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a1, a2});
 513       REQUIRE(insertion.has_value());
 514       REQUIRE(insertion.value() == PartialExecution{});
 515     }
 516   }
 517
 518   SECTION("Match against empty executions")
 519   {
 520     SECTION("Empty `v` trivially yields `w`")
 521     {
 522       auto insertion =
 523           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
 524       REQUIRE(insertion.has_value());
 525       REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
 526
 527       insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
 528       REQUIRE(insertion.has_value());
 529       REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
 530     }
 531
 532     SECTION("Empty `w` yields empty execution")
 533     {
 534       auto insertion =
 535           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a4, a5}, PartialExecution{});
 536       REQUIRE(insertion.has_value());
 537       REQUIRE(insertion.value() == PartialExecution{});
 538
 539       insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a5, a2}, PartialExecution{});
 540       REQUIRE(insertion.has_value());
 541       REQUIRE(insertion.value() == PartialExecution{});
 542     }
 543   }
 544 }