+ /* DPOR persistent set procedure:
+ * for each new transition considered, check if it depends on any other previous transition executed before it
+ * on another process. If there exists one, find the more recent, and add its process to the interleave set.
+ * If the process is not enabled at this point, then add every enabled process to the interleave */
+ if (reduction_mode_ == ReductionMode::dpor) {
+ aid_t issuer_id = state->get_transition_out()->aid_;
+ stack_t tmp_stack = stack_;
+ while (not tmp_stack.empty()) {
+ if (const State* prev_state = tmp_stack.back().get();
+ state->get_transition_out()->aid_ == prev_state->get_transition_out()->aid_) {
+ XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition_out()->to_string().c_str(),
+ prev_state->get_transition_out()->to_string().c_str(), issuer_id);
+ tmp_stack.pop_back();
+ continue;
+ } else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) {
+ XBT_VERB("Dependent Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+
+ if (prev_state->is_actor_enabled(issuer_id)) {
+ if (not prev_state->is_actor_done(issuer_id)) {
+ prev_state->consider_one(issuer_id);
+ opened_states_.emplace_back(tmp_stack.back());
+ } else
+ XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
+ } else {
+ XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled "
+ "transition as todo",
+ issuer_id);
+ // If we ended up marking at least a transition, explore it at some point
+ if (prev_state->consider_all() > 0)
+ opened_states_.emplace_back(tmp_stack.back());
+ }
+ break;
+ } else {
+ XBT_VERB("INDEPENDENT Transitions:");
+ XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
+ }
+ tmp_stack.pop_back();
+ }
+ } else if (reduction_mode_ == ReductionMode::sdpor) {
+ /**
+ * SDPOR Source Set Procedure:
+ *
+ * Find "reversible races" in the current execution with respect
+ * to the latest action `p`. For each such race, determine one thread
+ * not contained in the backtrack set at the "race point" `r` which
+ * "represents" the trace formed by first executing everything after
+ * `r` and then `p` to flip the race
+ */
+ execution_seq_.push_transition(executed_transition.get());
+
+ xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
+ "No events are contained in the SDPOR/OPDPOR execution "
+ "even though one was just added");
+ const aid_t p = executed_transition->aid_;
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+
+ for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) {
+ // To determine if the race is reversible, we have to ensure
+ // that actor `p` running `next_E_p` (viz. the event such that
+ // `racing_event -> (E_p) next_E_p` and no other event
+ // "happens-between" the two) is enabled in any equivalent
+ // execution where `racing_event` happens before `next_E_p`.
+ //
+ // Importantly, it is equivalent to checking if in ANY
+ // such equivalent execution sequence where `racing_event`
+ // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
+ // Thus it suffices to check THIS execution
+ //
+ // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
+ const std::shared_ptr<State> prev_state = stack_[racing_event_handle];
+ if (prev_state->is_actor_enabled(p)) {
+ // NOTE: To incorporate the idea of attempting to select the "best"
+ // backtrack point into SDPOR, instead of selecting the `first` initial,
+ // we should instead compute all choices and decide which is bes
+ const std::optional<aid_t> q =
+ execution_seq_.get_first_ssdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
+ if (q.has_value()) {
+ prev_state->consider_one(q.value());
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ }
+ }
+ }
+
+ // Before leaving that state, if the transition we just took can be taken multiple times, we
+ // need to give it to the opened states
+ if (stack_.back()->count_todo_multiples() > 0)
+ opened_states_.emplace_back(stack_.back());