for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
// TODO: We have to be able to react appropriately here when adding new
// types of transitions (multiple choices can be made :( )
- if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution(v, astate.get_transition(0))) {
+ if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
return v;
}
}
return std::nullopt;
}
-bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const
+bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const
{
auto E_w = *this;
std::vector<EventHandle> w_handles;
return false;
}
-bool Execution::is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
+bool Execution::is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
{
// INVARIANT: Here, we assume that for any process `p_i` of `w`,
// the events of this execution followed by the execution of all
const aid_t p = next_E_p->aid_;
// Is `p in `I_[E](w)`?
- if (E_v.is_initial_after_execution(w_now, p)) {
+ if (E_v.is_initial_after_execution_of(w_now, p)) {
// Remove `p` from w and continue
// TODO: If `p` occurs in `w`, it had better refer to the same
w_now.erase(action_by_p_in_w);
}
// Is `E ⊢ p ◇ w`?
- else if (E_v.is_independent_with_execution(w, next_E_p)) {
+ else if (E_v.is_independent_with_execution_of(w, next_E_p)) {
// INVARIANT: Note that it is impossible for `p` to be
// excluded from the set `I_[E](w)` BUT ALSO be contained in
// `w` itself if `E ⊢ p ◇ w`. We assert this is the case here
execution.push_transition(a4);
execution.push_transition(a5);
}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
+{
+ SECTION("Complete independence")
+ {
+ // Every transition is independent with every other and run by different actors. Hopefully
+ // we say that the events are independent with each other...
+ const auto a0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 5);
+ const auto a5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 6);
+ const auto a6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
+ const auto a7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6));
+
+ // In this case, we notice that `a6` and `a7` are executed by the same actor.
+ // Hence, a6 cannot be independent with extending the execution with a4.a5.a7.
+ // Notice that we are treating *a6* as the next step of actor 7 (that is what we
+ // supplied as an argument)
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6));
+ }
+
+ SECTION("Dependencies stopping independence from being possible")
+ {
+ const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a8 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+
+ // We see that although `a4` comes after `a1` with which it is dependent, it
+ // would come before "a6" in the partial execution `w`, so it would not be independent
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4));
+
+ // Removing `a6` from the picture, though, gives us the independence we're looking for.
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4));
+
+ // BUT, we we ask about a transition which is run by the same actor, even if they would be
+ // independent otherwise, we again lose independence
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4));
+
+ // This is a more interesting case:
+ // `indep` clearly is independent with the rest of the series, even though
+ // there are dependencies among the other events in the partial execution
+ REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep));
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
+{
+ const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+
+ SECTION("Equivalent insertions")
+ {
+ // TODO: Is this even a sensible question to ask if the two sequences
+ // don't agree upon what each actor executed after `E`?
+ const auto insertion =
+ Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{});
+ }
+
+ SECTION("")
+ {
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+ execution.push_transition(a5);
+ }
+}
