X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0a82e90d4cfdd7e27e1b946d22aff74a5abdda99..af53a6d1fbdda6d8d5523d1284927e8c72e24f91:/src/mc/SafetyChecker.cpp diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 4064b6aaf4..e223f5e4e4 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -268,7 +268,7 @@ int SafetyChecker::backtrack() XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); - simgrid::mc::replay(stack_); + this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size()); break; @@ -280,6 +280,31 @@ int SafetyChecker::backtrack() return SIMGRID_MC_EXIT_SUCCESS; } +void SafetyChecker::restoreState() +{ + /* Intermediate backtracking */ + { + simgrid::mc::State* state = stack_.back().get(); + if (state->system_state) { + simgrid::mc::restore_snapshot(state->system_state); + return; + } + } + + /* Restore the initial state */ + simgrid::mc::session->restoreInitialState(); + + /* Traverse the stack from the state at position start and re-execute the transitions */ + for (std::unique_ptr const& state : stack_) { + if (state == stack_.back()) + break; + session->execute(state->transition); + /* Update statistics */ + mc_model_checker->visited_states++; + mc_model_checker->executed_transitions++; + } +} + void SafetyChecker::init() { reductionMode_ = simgrid::mc::reduction_mode;