[mc] Move mc_stats.expanded_states into the Checkers

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index e5b383d..0e29e9a 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -344,7 +344,7 @@ void CommunicationDeterminismChecker::logState() // override
     XBT_INFO("******************************************************");
     XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
   }
-  XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
   XBT_INFO("Visited states = %lu", mc_stats->visited_states);
   XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
   if (simgrid::mc::initial_global_state != nullptr)
@@ -376,7 +376,7 @@ void CommunicationDeterminismChecker::prepare()
   }
 
   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("********* Start communication determinism verification *********");
 
@@ -455,7 +455,7 @@ int CommunicationDeterminismChecker::main(void)
 
       /* 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 comm determinism verification, we cannot stop the exploration if
          some communications are not finished (at least, data are transfered).
@@ -465,7 +465,8 @@ int CommunicationDeterminismChecker::main(void)
         && initial_global_state->initial_communications_pattern_done;
 
       if (_sg_mc_visited == 0
-          || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
+          || (visited_state = visitedStates_.addVisitedState(
+            expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())

diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
index 291d98e..781c2ba 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.hpp
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -34,6 +34,7 @@ private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;
   simgrid::mc::VisitedStates visitedStates_;
+  unsigned long expandedStatesCount_ = 0;
 };
 
 #endif

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index e5613cd..e3688e2 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -438,7 +438,7 @@ std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton
 {
   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->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
   next_pair->atomic_propositions = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;

diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index 3cbfce3..128722b 100644 (file)
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -89,6 +89,7 @@ private:
   std::list<std::shared_ptr<VisitedPair>> visitedPairs_;
   unsigned long visitedPairsCount_ = 0;
   unsigned long expandedPairsCount_ = 0;
+  unsigned long expandedStatesCount_ = 0;
 };
 
 }

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index b51d39a..e59dd97 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -90,7 +90,7 @@ std::vector<std::string> SafetyChecker::getTextualTrace() // override
 void SafetyChecker::logState() // override
 {
   Checker::logState();
-  XBT_INFO("Expanded states = %lu", mc_stats->expanded_states);
+  XBT_INFO("Expanded states = %lu", expandedStatesCount_);
   XBT_INFO("Visited states = %lu", mc_stats->visited_states);
   XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
 }
@@ -142,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();
@@ -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");

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index a9662be..71b5f67 100644 (file)
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -38,6 +38,7 @@ private:
   std::list<std::unique_ptr<simgrid::mc::State>> stack_;
   simgrid::mc::VisitedStates visitedStates_;
   std::unique_ptr<simgrid::mc::VisitedState> visitedState_;
+  unsigned long expandedStatesCount_ = 0;
 };
 
 }

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 746a0f1..6d0e87e 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -39,7 +39,7 @@ static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::Visi
  * \brief Save the current state
  * \return Snapshot of the current state.
  */
-VisitedState::VisitedState()
+VisitedState::VisitedState(unsigned long state_number)
 {
   simgrid::mc::Process* process = &(mc_model_checker->process());
   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
@@ -49,8 +49,8 @@ VisitedState::VisitedState()
   this->nb_processes =
     mc_model_checker->process().simix_processes().size();
 
-  this->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
-  this->num = mc_stats->expanded_states;
+  this->system_state = simgrid::mc::take_snapshot(state_number);
+  this->num = state_number;
   this->other_num = -1;
 }
 
@@ -76,10 +76,11 @@ void VisitedStates::prune()
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
-std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots)
+std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(
+  unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots)
 {
   std::unique_ptr<simgrid::mc::VisitedState> new_state =
-    std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
+    std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState(state_number));
   graph_state->system_state = new_state->system_state;
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)",
     new_state->system_state.get(), new_state->num, graph_state->num);

diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
index 364c8bf..13691af 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -23,7 +23,7 @@ struct XBT_PRIVATE VisitedState {
   int num = 0;
   int other_num = 0; // dot_output for
 
-  VisitedState();
+  VisitedState(unsigned long state_number);
   ~VisitedState();
 };
 
@@ -31,7 +31,7 @@ class XBT_PRIVATE VisitedStates {
   std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
 public:
   void clear() { states_.clear(); }
-  std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots);
+  std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots);
 private:
   void prune();
 };

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

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 8f675cf..50df4a3 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -28,13 +28,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
 /**
  * \brief Creates a state data structure used by the exploration algorithm
  */
-simgrid::mc::State* MC_state_new()
+simgrid::mc::State* MC_state_new(unsigned long state_number)
 {
   simgrid::mc::State* state = new simgrid::mc::State();
   state->processStates.resize(MC_smx_get_maxpid());
-  state->num = ++mc_stats->expanded_states;
+  state->num = state_number;
   /* Stateful model checking */
-  if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
+  if((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) ||  _sg_mc_termination){
     state->system_state = simgrid::mc::take_snapshot(state->num);
     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
       MC_state_copy_incomplete_communications_pattern(state);

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 43554bf..599b0cb 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -151,7 +151,7 @@ XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& st
 }
 }
 
-XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
+XBT_PRIVATE simgrid::mc::State* MC_state_new(unsigned long state_number);
 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
 
 #endif