[mc] Move liveness stats out of mc_stats into LivenessChecker

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 15a0a73..e5613cd 100644 (file)
--- 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++;
@@ -304,8 +304,8 @@ RecordTrace LivenessChecker::getRecordTrace() // override
 void LivenessChecker::logState() // override
 {
   Checker::logState();
-  XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs);
-  XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs);
+  XBT_INFO("Expanded pairs = %lu", expandedPairsCount_);
+  XBT_INFO("Visited pairs = %lu", visitedPairsCount_);
   XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
 }
 
@@ -402,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);
@@ -436,7 +436,7 @@ int LivenessChecker::main(void)
 
 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);

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index 2c482ad..f9def21 100644 (file)
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -38,7 +38,7 @@ struct XBT_PRIVATE Pair {
   int depth = 0;
   bool exploration_started = false;
 
-  Pair();
+  Pair(unsigned long expanded_pairs);
   ~Pair();
 
   Pair(Pair const&) = delete;
@@ -87,6 +87,9 @@ public:
   std::list<std::shared_ptr<Pair>> explorationStack_;
   std::list<std::shared_ptr<VisitedPair>> acceptancePairs_;
   std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
+private:
+  unsigned long visitedPairsCount_ = 0;
+  unsigned long expandedPairsCount_ = 0;
 };
 
 }

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 143aac7..8308388 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -69,9 +69,7 @@ XBT_PRIVATE void MC_show_deadlock(void);
 typedef struct mc_stats {
   unsigned long state_size;
   unsigned long visited_states;
-  unsigned long visited_pairs;
   unsigned long expanded_states;
-  unsigned long expanded_pairs;
   unsigned long executed_transitions;
 } s_mc_stats_t, *mc_stats_t;