[mc] Remove mc_stats and move remaining stats in ModelChecker for now

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index b51d39a..5e106ad 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -90,9 +90,9 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
 void SafetyChecker::logState() // override
 {
   Checker::logState();
-  XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
-  XBT_INFO("Visited states = %lu", mc_stats->visited_states);
-  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 }
 
 int SafetyChecker::run()
@@ -110,7 +110,7 @@ int SafetyChecker::run()
       stack_.size(), state, state->num,
       state->interleaveSize());
 
-    mc_stats->visited_states++;
+    mc_model_checker->visited_states++;
 
     // The interleave set is empty or the maximum depth is reached,
     // let's back-track.
@@ -135,14 +135,14 @@ int SafetyChecker::run()
     if (dot_output != nullptr)
       req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
 
-    mc_stats->executed_transitions++;
+    mc_model_checker->executed_transitions++;
 
     /* Answer the request */
     this->getSession().execute(state->transition);
 
     /* Create the new expanded state */
     std::unique_ptr<simgrid::mc::State> next_state =
-      std::unique_ptr<simgrid::mc::State>(MC_state_new());
+      std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
     if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
         MC_show_non_termination();
@@ -150,7 +150,7 @@ int SafetyChecker::run()
     }
 
     if (_sg_mc_visited == 0
-        || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
+        || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
 
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto& p : mc_model_checker->process().simix_processes())
@@ -298,7 +298,7 @@ void SafetyChecker::init()
   XBT_DEBUG("Starting the safety algorithm");
 
   std::unique_ptr<simgrid::mc::State> initial_state =
-    std::unique_ptr<simgrid::mc::State>(MC_state_new());
+    std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");