// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
// happen after `e` is a member of `v`. In addition to marking
// the event in `v`, we also "simulate" running the action `v`
// from E'
// happen after `e` is a member of `v`. In addition to marking
// the event in `v`, we also "simulate" running the action `v`
// from E'
// First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
// First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
"For any non-empty execution, we know that "
"at minimum one actor is an initial since "
"some execution is possible with respect to a "
"For any non-empty execution, we know that "
"at minimum one actor is an initial since "
"some execution is possible with respect to a "
// Remove `p` from w and continue
// INVARIANT: If `p` occurs in `w`, it had better refer to the same
// Remove `p` from w and continue
// INVARIANT: If `p` occurs in `w`, it had better refer to the same