//
// Note the form of `v` in the pseudocode:
// `v := notdep(e, E).e'^
- {
- E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
- v.push_back(get_event_with_handle(e_prime).get_transition());
-
- const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
- v_handles.push_back(e_prime_in_E_prime_v);
-
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
- });
- if (is_initial) {
- if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
- return std::nullopt;
- } else {
- WI_E_prime_v.insert(q);
- }
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ v.push_back(get_event_with_handle(e_prime).get_transition());
+
+ const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+ v_handles.push_back(e_prime_in_E_prime_v);
+
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
+ return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
+ });
+ if (is_initial) {
+ if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
+ return std::nullopt;
+ } else {
+ WI_E_prime_v.insert(q);
}
}
- {
- const Execution pre_E_e = get_prefix_before(e);
- const auto sleeping_actors = state_at_e.get_sleeping_actors();
-
- // Check if any enabled actor that is independent with
- // this execution after `v` is contained in the sleep set
- for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
- const bool is_in_WI_E =
- astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
- const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
-
- // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
- // This implies that the intersection between the two is non-empty
- if (is_in_WI_E && is_in_sleep_set) {
- return std::nullopt;
- }
- }
+
+ const Execution pre_E_e = get_prefix_before(e);
+ const auto sleeping_actors = state_at_e.get_sleeping_actors();
+
+ // Check if any enabled actor that is independent with
+ // this execution after `v` is contained in the sleep set
+ for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
+ const bool is_in_WI_E =
+ astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
+ const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
+
+ // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
+ // This implies that the intersection between the two is non-empty
+ if (is_in_WI_E && is_in_sleep_set)
+ return std::nullopt;
}
+
return v;
}
return subset_local;
}();
- {
- // To test this, we verify that at each point none of the events
- // that follow after any particular event `e` are contained in
- // `e`'s history
- EventSet invalid_events = subset;
- const auto ordered_events = subset.get_topological_ordering();
-
- std::for_each(ordered_events.begin(), ordered_events.end(), [&](const UnfoldingEvent* e) {
- History history(e);
- for (const auto* e_hist : history) {
- if (e_hist == e)
- continue;
- REQUIRE_FALSE(invalid_events.contains(e_hist));
- }
- invalid_events.remove(e);
- });
+ // To test this, we verify that at each point none of the events
+ // that follow after any particular event `e` are contained in
+ // `e`'s history
+ EventSet invalid_events = subset;
+ for (const auto* e : subset.get_topological_ordering()) {
+ for (const auto* e_hist : History(e)) {
+ if (e_hist == e)
+ continue;
+ REQUIRE_FALSE(invalid_events.contains(e_hist));
+ }
+ invalid_events.remove(e);
}
- {
- // To test this, we verify that at each point none of the events
- // that we've processed in the ordering are ever seen again
- // in anybody else's history
- EventSet events_seen;
- const auto ordered_events = subset.get_topological_ordering_of_reverse_graph();
-
- std::for_each(ordered_events.begin(), ordered_events.end(), [&events_seen](const UnfoldingEvent* e) {
- History history(e);
-
- for (const auto* e_hist : history) {
- // Unlike the test above, we DO want to ensure
- // that `e` itself ALSO isn't yet seen
-
- // If this event has been "seen" before,
- // this implies that event `e` appears later
- // in the list than one of its ancestors
- REQUIRE_FALSE(events_seen.contains(e_hist));
- }
- events_seen.insert(e);
- });
+
+ // To test this, we verify that at each point none of the events
+ // that we've processed in the ordering are ever seen again
+ // in anybody else's history
+ EventSet events_seen;
+ for (const auto* e : subset.get_topological_ordering_of_reverse_graph()) {
+ for (const auto* e_hist : History(e)) {
+ // Unlike the test above, we DO want to ensure
+ // that `e` itself ALSO isn't yet seen
+
+ // If this event has been "seen" before,
+ // this implies that event `e` appears later
+ // in the list than one of its ancestors
+ REQUIRE_FALSE(events_seen.contains(e_hist));
+ }
+ events_seen.insert(e);
}
}
}
// --- ex({⊥}) ---
const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_send);
- { // Assert that event `a` has been added
- UnfoldingEvent e_send(EventSet(), comm_send);
- REQUIRE(incremental_exC_send.size() == 1);
- REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
- REQUIRE(U.size() == 1);
- }
+ // Assert that event `a` has been added
+ UnfoldingEvent e_send(EventSet(), comm_send);
+ REQUIRE(incremental_exC_send.size() == 1);
+ REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
+ REQUIRE(U.size() == 1);
const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_recv);
- { // Assert that event `b` has been added
- UnfoldingEvent e_recv(EventSet(), comm_recv);
- REQUIRE(incremental_exC_recv.size() == 1);
- REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
- REQUIRE(U.size() == 2);
- }
+ // Assert that event `b` has been added
+ UnfoldingEvent e_recv(EventSet(), comm_recv);
+ REQUIRE(incremental_exC_recv.size() == 1);
+ REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
+ REQUIRE(U.size() == 2);
// --- ex({⊥}) ---
// 2. UDPOR will then attempt to expand ex({⊥, a}) or ex({⊥, b}). Both have
// --- ex({⊥, a}) ---
const auto incremental_exC_recv2 = ExtensionSetCalculator::partially_extend(Configuration({e_a}), &U, comm_recv);
- { // Assert that no event has been added and that
- // e_b is contained in the extension set
- UnfoldingEvent e_send(EventSet(), comm_send);
- REQUIRE(incremental_exC_recv2.size() == 1);
- REQUIRE(incremental_exC_recv2.contains(e_b));
+ // Assert that no event has been added and that
+ // e_b is contained in the extension set
+ REQUIRE(incremental_exC_recv2.size() == 1);
+ REQUIRE(incremental_exC_recv2.contains(e_b));
- // Here, `e_a` shouldn't be added again
- REQUIRE(U.size() == 2);
- }
+ // Here, `e_a` shouldn't be added again
+ REQUIRE(U.size() == 2);
// --- ex({⊥, a}) ---
// --- ex({⊥, b}) ---
const auto incremental_exC_send2 = ExtensionSetCalculator::partially_extend(Configuration({e_b}), &U, comm_send);
- { // Assert that no event has been added and that
- // e_a is contained in the extension set
- REQUIRE(incremental_exC_send2.size() == 1);
- REQUIRE(incremental_exC_send2.contains(e_a));
+ // Assert that no event has been added and that
+ // e_a is contained in the extension set
+ REQUIRE(incremental_exC_send2.size() == 1);
+ REQUIRE(incremental_exC_send2.contains(e_a));
- // Here, `e_b` shouldn't be added again
- REQUIRE(U.size() == 2);
- }
+ // Here, `e_b` shouldn't be added again
+ REQUIRE(U.size() == 2);
// --- ex({⊥, b}) ---
// 3. Expanding from ex({⊥, a, b}) brings in both `CommWait` events since they
// --- ex({⊥, a, b}) ---
const auto incremental_exC_wait_actor_1 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_1);
- { // Assert that events `c` has been added
- UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
- REQUIRE(incremental_exC_wait_actor_1.size() == 1);
- REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
- REQUIRE(U.size() == 3);
- }
+ // Assert that events `c` has been added
+ UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
+ REQUIRE(incremental_exC_wait_actor_1.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
+ REQUIRE(U.size() == 3);
const auto incremental_exC_wait_actor_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_2);
- { // Assert that events `d` has been added
- UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
- REQUIRE(incremental_exC_wait_actor_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
- REQUIRE(U.size() == 4);
- }
+ // Assert that events `d` has been added
+ UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
+ REQUIRE(incremental_exC_wait_actor_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b}) ---
// 4. Expanding from either wait action should simply yield the other event
// --- ex({⊥, a, b, d}) ---
const auto incremental_exC_wait_actor_1_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_d}), &U, comm_wait_1);
- { // Assert that no event has been added and that
- // `e_c` is contained in the extension set
- REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
- REQUIRE(U.size() == 4);
- }
+ // Assert that no event has been added and that
+ // `e_c` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b, d}) ---
// --- ex({⊥, a, b, c}) ---
const auto incremental_exC_wait_actor_2_2 =
ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_c}), &U, comm_wait_2);
- { // Assert that no event has been added and that
- // `e_d` is contained in the extension set
- REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
- REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
- REQUIRE(U.size() == 4);
- }
+ // Assert that no event has been added and that
+ // `e_d` is contained in the extension set
+ REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
+ REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
+ REQUIRE(U.size() == 4);
// --- ex({⊥, a, b, c}) ---
-}
\ No newline at end of file
+}
