#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
+TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Semantic Equivalence Tests")
+{
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e3(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e4(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ UnfoldingEvent e5(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e6(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e7(EventSet({&e1, &e3, &e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+
+ SECTION("Equivalence is an equivalence relation")
+ {
+ SECTION("Equivalence is reflexive")
+ {
+ REQUIRE(e1 == e1);
+ REQUIRE(e2 == e2);
+ REQUIRE(e3 == e3);
+ REQUIRE(e4 == e4);
+ }
+
+ SECTION("Equivalence is symmetric")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e2);
+ REQUIRE(e3 == e4);
+ REQUIRE(e4 == e3);
+ REQUIRE(e2 == e4);
+ REQUIRE(e4 == e2);
+ }
+
+ SECTION("Equivalence is transitive")
+ {
+ REQUIRE(e2 == e3);
+ REQUIRE(e3 == e4);
+ REQUIRE(e2 == e4);
+ REQUIRE(e5 == e6);
+ REQUIRE(e6 == e7);
+ REQUIRE(e5 == e7);
+ }
+ }
+
+ SECTION("Equivalence fails with different actors")
+ {
+ UnfoldingEvent e1_diff_actor(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e2_diff_actor(EventSet({&e1}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ UnfoldingEvent e5_diff_actor(EventSet({&e1, &e3, &e2}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1, 0));
+ REQUIRE(e1 != e1_diff_actor);
+ REQUIRE(e1 != e2_diff_actor);
+ REQUIRE(e1 != e5_diff_actor);
+ }
+
+ SECTION("Equivalence fails with different transition types")
+ {
+ // NOTE: We're comparing the transition `type_` field directly. To avoid
+ // modifying the `Type` enum that exists in `Transition` just for the tests,
+ // we instead provide different values of `Transition::Type` to simulate
+ // the different types
+ UnfoldingEvent e1_diff_transition(EventSet(),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e2_diff_transition(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ UnfoldingEvent e5_diff_transition(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::ACTOR_JOIN, 0, 0));
+ REQUIRE(e1 != e1_diff_transition);
+ REQUIRE(e1 != e2_diff_transition);
+ REQUIRE(e1 != e5_diff_transition);
+ }
+
+ SECTION("Equivalence fails with different `times_considered`")
+ {
+ // With a different number for `times_considered`, we know
+ UnfoldingEvent e1_diff_considered(EventSet(), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e2_diff_considered(EventSet({&e1}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ UnfoldingEvent e5_diff_considered(EventSet({&e1, &e3, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 1));
+ REQUIRE(e1 != e1_diff_considered);
+ REQUIRE(e1 != e2_diff_considered);
+ REQUIRE(e1 != e5_diff_considered);
+ }
+
+ SECTION("Equivalence fails with different immediate histories of events")
+ {
+ UnfoldingEvent e1_diff_hist(EventSet({&e2}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e2_diff_hist(EventSet({&e3}), std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ UnfoldingEvent e5_diff_hist(EventSet({&e1, &e2}),
+ std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 0, 0));
+ REQUIRE(e1 != e1_diff_hist);
+ REQUIRE(e1 != e2_diff_hist);
+ REQUIRE(e1 != e5_diff_hist);
+ }
+}
+
TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Dependency/Conflict Tests")
{
SECTION("Properties of the relations")
UnfoldingEvent e1(EventSet(), std::make_shared<ConditionallyDependentAction>());
UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>());
UnfoldingEvent e3(EventSet({&e2}), std::make_shared<IndependentAction>());
- UnfoldingEvent e4(EventSet({&e3}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e4(EventSet({&e3}), std::make_shared<ConditionallyDependentAction>());
UnfoldingEvent e5(EventSet({&e3}), std::make_shared<DependentAction>());
UnfoldingEvent e6(EventSet({&e1}), std::make_shared<ConditionallyDependentAction>());
UnfoldingEvent e7(EventSet({&e6, &e2}), std::make_shared<ConditionallyDependentAction>());
REQUIRE_FALSE(e5.conflicts_with(&e5));
REQUIRE_FALSE(e6.conflicts_with(&e6));
REQUIRE_FALSE(e7.conflicts_with(&e7));
+
+ REQUIRE_FALSE(e1.immediately_conflicts_with(&e1));
+ REQUIRE_FALSE(e2.immediately_conflicts_with(&e2));
+ REQUIRE_FALSE(e3.immediately_conflicts_with(&e3));
+ REQUIRE_FALSE(e4.immediately_conflicts_with(&e4));
+ REQUIRE_FALSE(e5.immediately_conflicts_with(&e5));
+ REQUIRE_FALSE(e6.immediately_conflicts_with(&e6));
+ REQUIRE_FALSE(e7.immediately_conflicts_with(&e7));
}
SECTION("Conflict relation is symmetric")
{
REQUIRE(e5.conflicts_with(&e6));
REQUIRE(e6.conflicts_with(&e5));
+ REQUIRE(e5.immediately_conflicts_with(&e4));
+ REQUIRE(e4.immediately_conflicts_with(&e5));
}
}
}
CHECK_FALSE(e7.conflicts_with(&e6));
CHECK_FALSE(e7.conflicts_with(&e7));
}
+}
+
+TEST_CASE("simgrid::mc::udpor::UnfoldingEvent: Immediate Conflicts + Conflicts Stress Test")
+{
+ // The following tests concern the given event structure:
+ // e1
+ // / / /
+ // e2 e3 e4
+ // / / /
+ // e5 e10
+ // /
+ // e6
+ // / /
+ // e7 e8
+ // /
+ // e9
+ //
+ // Immediate conflicts:
+ // e2 + e3
+ // e3 + e4
+ // e2 + e4
+ //
+ // NOTE: e7 + e8 ARE NOT in immediate conflict! The reason is that
+ // the set of events {e8, e6, e5, e3, e4, e1} is not a valid configuration,
+ // (nor is {e7, e6, e5, e3, e4, e1})
+ //
+ // NOTE: e2/e3 + e10 are NOT in immediate conflict! EVEN THOUGH {e1, e4, e10}
+ // is a valid configuration, {e1, e2/e3, e4} is not (since e2/e3 and e4 conflict)
+ UnfoldingEvent e1(EventSet(), std::make_shared<IndependentAction>());
+ UnfoldingEvent e2(EventSet({&e1}), std::make_shared<DependentAction>());
+ UnfoldingEvent e3(EventSet({&e1}), std::make_shared<DependentAction>());
+ UnfoldingEvent e4(EventSet({&e1}), std::make_shared<DependentAction>());
+ UnfoldingEvent e5(EventSet({&e3, &e4}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e6(EventSet({&e5}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e7(EventSet({&e6}), std::make_shared<DependentAction>());
+ UnfoldingEvent e8(EventSet({&e6}), std::make_shared<DependentAction>());
+ UnfoldingEvent e9(EventSet({&e8}), std::make_shared<IndependentAction>());
+ UnfoldingEvent e10(EventSet({&e4}), std::make_shared<DependentAction>());
+
+ REQUIRE(e2.immediately_conflicts_with(&e3));
+ REQUIRE(e3.immediately_conflicts_with(&e4));
+ REQUIRE(e2.immediately_conflicts_with(&e4));
+
+ REQUIRE(e2.conflicts_with(&e10));
+ REQUIRE(e3.conflicts_with(&e10));
+ REQUIRE(e7.conflicts_with(&e8));
+ REQUIRE_FALSE(e2.immediately_conflicts_with(&e10));
+ REQUIRE_FALSE(e3.immediately_conflicts_with(&e10));
+ REQUIRE_FALSE(e7.immediately_conflicts_with(&e8));
}
\ No newline at end of file
