+
+ SECTION("Example 3: Happens-before is transitively-closed")
+ {
+ // Given a reversible race between events `e1` and `e3` in a simulation,
+ // we assert that `e5` would be eliminated from being contained in
+ // the sequence `notdep(e1, E)`
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_transition(e0);
+ execution.push_transition(e1);
+ execution.push_transition(e2);
+ execution.push_transition(e3);
+ execution.push_transition(e4);
+
+ REQUIRE(execution.happens_before(0, 2));
+ REQUIRE(execution.happens_before(2, 4));
+ REQUIRE(execution.happens_before(0, 4));
+ }