std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
std::unordered_set<Execution::EventHandle> disqualified_events;
// For each event of the execution
for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
// We need `e_i -->_E target` as a necessary condition
if (not happens_before(e_i, target)) {
std::unordered_set<Execution::EventHandle> disqualified_events;
// For each event of the execution
for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
// We need `e_i -->_E target` as a necessary condition
if (not happens_before(e_i, target)) {
continue;
}
// Further, `proc(e_i) != proc(target)`
if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
disqualified_events.insert(e_i);
continue;
}
// Further, `proc(e_i) != proc(target)`
if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
disqualified_events.insert(e_i);
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)",
+ target, e_i, e_j, e_i, e_j, target);
// it (since this would transitively make it the event
// which "happens-between" `target` and `e`)
if (disqualified_events.count(e_i) == 0) {
// it (since this would transitively make it the event
// which "happens-between" `target` and `e`)
if (disqualified_events.count(e_i) == 0) {
E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
v.push_back(get_event_with_handle(e_star).get_transition());
E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
v.push_back(get_event_with_handle(e_star).get_transition());
const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
// When checking whether any event in `dom_[E'](v)` happens before
const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
// When checking whether any event in `dom_[E'](v)` happens before
- 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_star_in_E_prime_v);
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_star_in_E_prime_v);
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 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);
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_prime_in_E_prime_v);