X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0433449947b08247ca57c84e32f547c35e351145..cadc6f2a1e9eea38f5b9cd5f148e1bc282c26981:/src/mc/LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 537dd9bf74..e5613cd6bf 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -94,7 +94,7 @@ static bool evaluate_label(
   }
 }
 
-Pair::Pair() : num(++mc_stats->expanded_pairs)
+Pair::Pair(unsigned long expanded_pairs) : num(expanded_pairs)
 {}
 
 Pair::~Pair() {}
@@ -223,7 +223,7 @@ void LivenessChecker::replay()
     }
 
     /* Update statistics */
-    mc_stats->visited_pairs++;
+    visitedPairsCount_++;
     mc_stats->executed_transitions++;
 
     depth++;
@@ -301,6 +301,14 @@ RecordTrace LivenessChecker::getRecordTrace() // override
   return res;
 }
 
+void LivenessChecker::logState() // override
+{
+  Checker::logState();
+  XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+  XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
+  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+}
+
 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
 {
   XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
@@ -310,7 +318,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth)
   simgrid::mc::dumpRecordPath();
   for (auto& s : this->getTextualTrace())
     XBT_INFO("%s", s.c_str());
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   XBT_INFO("Counter-example depth : %zd", depth);
 }
 
@@ -394,7 +402,7 @@ int LivenessChecker::main(void)
     /* Update mc_stats */
     mc_stats->executed_transitions++;
     if (!current_pair->exploration_started)
-      mc_stats->visited_pairs++;
+      visitedPairsCount_++;
 
     /* Answer the request */
     mc_model_checker->handle_simcall(current_pair->graph_state->transition);
@@ -422,13 +430,13 @@ int LivenessChecker::main(void)
   }
 
   XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
+  simgrid::mc::session->logState();
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
 {
-  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
+  std::shared_ptr<Pair> next_pair = std::make_shared<Pair>(++expandedPairsCount_);
   next_pair->automaton_state = state;
   next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
   next_pair->atomic_propositions = std::move(propositions);