+ } else {
+ XBT_DEBUG("Event `%u` (%ld:%s) dismissed from the construction of v", e_star, get_actor_with_handle(e_star),
+ get_event_with_handle(e_star).get_transition()->to_string().c_str());
+ }
+ }
+
+ // Now we add `e_prime := <q, i>` to `E'.v` and repeat the same work
+ // It's possible `proc(e_prime)` is an initial
+ //
+ // 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& handle) {
+ return E_prime_v.happens_before(handle, 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;
+ }
+
+ return v;
+}
+
+bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const
+{
+ auto E_w = *this;
+ std::vector<EventHandle> w_handles;
+ for (const auto& w_i : w) {
+ // Take one step in the direction of `w`
+ E_w.push_transition(w_i);
+
+ // If that step happened to be executed by `p`,
+ // great: we know that `p` is contained in `w`.
+ // We now need to verify that it doens't "happen-after"
+ // any events which occur before it
+ if (w_i->aid_ == p) {
+ const auto p_handle = E_w.get_latest_event_handle().value();
+ return std::none_of(w_handles.begin(), w_handles.end(),
+ [&](const auto handle) { return E_w.happens_before(handle, p_handle); });
+ } else {
+ w_handles.push_back(E_w.get_latest_event_handle().value());
+ }
+ }
+ return false;
+}
+
+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
+ // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`)
+ // are sufficient to enable `p_i`. This is fortunately the case
+ // with what ODPOR requires of us, viz. to ask the question about
+ // `v := notdep(e, E)` for some execution `E` and event `e` of
+ // that execution.
+ auto E_p_w = *this;
+ E_p_w.push_transition(std::move(next_E_p));
+ const auto p_handle = E_p_w.get_latest_event_handle().value();
+
+ // As we add events to `w`, verify that none
+ // of them "happen-after" the event associated with
+ // the step `next_E_p` (viz. p_handle)
+ for (const auto& w_i : w) {
+ E_p_w.push_transition(w_i);
+ const auto w_i_handle = E_p_w.get_latest_event_handle().value();
+ if (E_p_w.happens_before(p_handle, w_i_handle)) {
+ return false;
+ }
+ }
+ return true;
+}
+
+std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) const
+{
+ // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically
+ // where the [iterative] computation of `v ~_[E] w` is described)
+ auto E_v = *this;
+ auto w_now = w;
+
+ for (const auto& next_E_p : v) {
+ // Is `p in `I_[E](w)`?
+ if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) {
+ // Remove `p` from w and continue
+
+ // INVARIANT: If `p` occurs in `w`, it had better refer to the same
+ // transition referenced by `v`. Unfortunately, we have two
+ // sources of truth here which can be manipulated at the same
+ // time as arguments to the function. If ODPOR works correctly,
+ // they should always refer to the same value; but as a sanity check,
+ // we have an assert that tests that at least the types are the same.
+ const auto action_by_p_in_w =
+ std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
+ xbt_assert(action_by_p_in_w != w_now.end(), "Invariant violated: actor `p` "
+ "is claimed to be an initial after `w` but is "
+ "not actually contained in `w`. This indicates that there "
+ "is a bug computing initials");
+ const auto& w_action = *action_by_p_in_w;
+ xbt_assert(w_action->type_ == next_E_p->type_,
+ "Invariant violated: `v` claims that actor `%ld` executes '%s' while "
+ "`w` claims that it executes '%s'. These two partial executions both "
+ "refer to `next_[E](p)`, which should be the same",
+ p, next_E_p->to_string(false).c_str(), w_action->to_string(false).c_str());
+ w_now.erase(action_by_p_in_w);
+ }
+ // Is `E ⊢ p ◇ w`?
+ else if (E_v.is_independent_with_execution_of(w_now, 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` (intuitively, the fact that `E ⊢ p ◇ w`
+ // means that are able to move `p` anywhere in `w` IF it occurred, so
+ // if it really does occur we know it must then be an initial).
+ // We assert this is the case here
+ const auto action_by_p_in_w =
+ std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
+ xbt_assert(action_by_p_in_w == w_now.end(),
+ "Invariant violated: We claimed that actor `%ld` is not an initial "
+ "after `w`, yet it's independent with all actions of `w` AND occurs in `w`."
+ "This indicates that there is a bug computing initials",
+ p);
+ } else {
+ // Neither of the two above conditions hold, so the relation fails
+ return std::nullopt;