[mc] Duplicate restoreState() as a method of SafetyChecker

* it is much simpler in this form;

* we should focus on making a nice Session API for SafetyChecker and
  then expand it for other algorithms.

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index a2ce9d4..e223f5e 100644 (file)
--- 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::restoreState(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<simgrid::mc::State> 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;

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index 71b5f67..b2dd269 100644 (file)
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -33,6 +33,7 @@ private:
   void init();
   bool checkNonTermination(simgrid::mc::State* current_state);
   int backtrack();
+  void restoreState();
 private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;