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

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 0e29e9a..0677f95 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -345,8 +345,8 @@ void CommunicationDeterminismChecker::logState() // override
     XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
   }
   XBT_INFO("Expanded states = %lu", expandedStatesCount_);
-  XBT_INFO("Visited states = %lu", mc_stats->visited_states);
-  XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+  XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
   if (simgrid::mc::initial_global_state != nullptr)
     XBT_INFO("Send-deterministic : %s",
       !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
@@ -418,7 +418,7 @@ int CommunicationDeterminismChecker::main(void)
               state->interleaveSize());
 
     /* Update statistics */
-    mc_stats->visited_states++;
+    mc_model_checker->visited_states++;
 
     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
         && (req = MC_state_get_request(state)) != nullptr
@@ -434,7 +434,7 @@ int CommunicationDeterminismChecker::main(void)
       if (dot_output != nullptr)
         req_str = simgrid::mc::request_get_dot_output(req, req_num);
 
-      mc_stats->executed_transitions++;
+      mc_model_checker->executed_transitions++;
 
       /* TODO : handle test and testany simcalls */
       e_mc_call_type_t call = MC_CALL_TYPE_NONE;

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index e3688e2..584337f 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -224,7 +224,7 @@ void LivenessChecker::replay()
 
     /* Update statistics */
     visitedPairsCount_++;
-    mc_stats->executed_transitions++;
+    mc_model_checker->executed_transitions++;
 
     depth++;
 
@@ -306,7 +306,7 @@ 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);
+  XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
 }
 
 void LivenessChecker::showAcceptanceCycle(std::size_t depth)
@@ -399,8 +399,8 @@ int LivenessChecker::main(void)
       simgrid::mc::request_to_string(
         req, req_num, simgrid::mc::RequestType::simix).c_str());
 
-    /* Update mc_stats */
-    mc_stats->executed_transitions++;
+    /* Update stats */
+    mc_model_checker->executed_transitions++;
     if (!current_pair->exploration_started)
       visitedPairsCount_++;
 

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 9aaffdd..b5baea4 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -111,9 +111,6 @@ void ModelChecker::start()
 
   process_->init();
 
-  /* Initialize statistics */
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
-
   if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
     MC_init_dot_output();
 

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index 394a8c1..6619f25 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -81,6 +81,9 @@ private:
   void handle_waitpid();
   void on_signal(const struct signalfd_siginfo* info);
 
+public:
+  unsigned long visited_states = 0;
+  unsigned long executed_transitions = 0;
 };
 
 }

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index e59dd97..5e106ad 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -91,8 +91,8 @@ 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);
+  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,7 +135,7 @@ 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);

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 630adb9..1213e1c 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -64,8 +64,6 @@ std::vector<double> processes_time;
 simgrid::mc::State* mc_current_state = nullptr;
 char mc_replay_mode = false;
 
-mc_stats_t mc_stats = nullptr;
-
 /* Liveness */
 
 namespace simgrid {
@@ -189,8 +187,8 @@ void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
     }
 
     /* Update statistics */
-    mc_stats->visited_states++;
-    mc_stats->executed_transitions++;
+    mc_model_checker->visited_states++;
+    mc_model_checker->executed_transitions++;
 
   }
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 235a5be..ad31323 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -64,15 +64,6 @@ XBT_PRIVATE extern FILE *dot_output;
 
 XBT_PRIVATE void MC_show_deadlock(void);
 
-/****************************** Statistics ************************************/
-
-typedef struct mc_stats {
-  unsigned long visited_states;
-  unsigned long executed_transitions;
-} s_mc_stats_t, *mc_stats_t;
-
-XBT_PRIVATE extern mc_stats_t mc_stats;
-
 /********************************** Snapshot comparison **********************************/
 
 //#define MC_DEBUG 1