- /* If this is a new state (or if we don't care about state-equality reduction) */
- if (visited_state_ == nullptr) {
- /* Get an enabled process and insert it in the interleave set of the next state */
- for (auto const& [aid, _] : next_state->get_actors_list()) {
- if (next_state->is_actor_enabled(aid)) {
- next_state->mark_todo(aid);
- if (reductionMode_ == ReductionMode::dpor)
- break; // With DPOR, we take the first enabled transition
+ /* 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(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+ prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+ 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(" #%ld %s (state=%ld)", prev_state->get_transition_out()->aid_,
+ prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
+ XBT_VERB(" #%ld %s (state=%ld)", state->get_transition_out()->aid_,
+ state->get_transition_out()->to_string().c_str(), state->get_num());