[mc] Move mc_stats.expanded_states into the Checkers

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

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 698b546..e59dd97 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -43,7 +43,7 @@ static void MC_show_non_termination(void)
   XBT_INFO("Counter-example execution trace:");
   for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
 }
 
 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
@@ -87,6 +87,14 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
   return trace;
 }
 
+void SafetyChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+  XBT_INFO("Visited states = %lu", mc_stats->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+}
+
 int SafetyChecker::run()
 {
   this->init();
@@ -134,7 +142,7 @@ int SafetyChecker::run()
 
     /* 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();
@@ -142,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())
@@ -165,7 +173,7 @@ int SafetyChecker::run()
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   initial_global_state = nullptr;
   return SIMGRID_MC_EXIT_SUCCESS;
 }
@@ -290,14 +298,11 @@ 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");
 
-  /* Wait for requests (schedules processes) */
-  mc_model_checker->wait_for_requests();
-
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {