- /* Traverse the stack backwards until a state with a non empty interleave
- set is found, deleting all the states that have it empty in the way.
- For each deleted state, check if the request that has generated it
- (from it's predecesor state), depends on any other previous request
- executed before it. If it does then add it to the interleave set of the
- state that executed that previous request. */
-
- while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
- if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
- req = MC_state_get_internal_request(state);
- if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
- xbt_die("Mutex is currently not supported with DPOR, "
- "use --cfg=model-check/reduction:none");
- const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
- xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) {
- if (reductionMode_ != simgrid::mc::ReductionMode::none
- && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
- if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
- XBT_DEBUG("Dependent Transitions:");
- smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
- XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
- xbt_free(req_str);
- prev_req = MC_state_get_executed_request(state, &value);
- req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
- XBT_DEBUG("%s (state=%d)", req_str, state->num);
- xbt_free(req_str);
- }
-
- if (!MC_state_process_is_done(prev_state, issuer))
- MC_state_interleave_process(prev_state, issuer);
- else
- XBT_DEBUG("Process %p is in done set", req->issuer);
-
- break;
-
- } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
-
- XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
- break;
-
- } else {
-
- const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
- XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
- req->call, issuer->pid, state->num,
- MC_state_get_internal_request(prev_state)->call,
- previous_issuer->pid,
- prev_state->num);
-
- }
- }
- }
+ if (state->interleaveSize()
+ && stack_.size() < (std::size_t) _sg_mc_max_depth) {
+ /* We found a back-tracking point, let's loop */
+ XBT_DEBUG("Back-tracking to state %d at depth %zi",
+ state->num, stack_.size() + 1);
+ stack_.push_back(std::move(state));
+ this->restoreState();
+ XBT_DEBUG("Back-tracking to state %d at depth %zi done",
+ stack_.back()->num, stack_.size());
+ break;
+ } else {
+ XBT_DEBUG("Delete state %d at depth %zi",
+ state->num, stack_.size() + 1);
+ }
+ }
+ return SIMGRID_MC_EXIT_SUCCESS;
+}