[mc] Move mc_stats.expanded_states into the Checkers

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index e5b383d922f3d2b7df01e7091beaa34cfd1cc745..0e29e9a0c470e0e9f2f6a6c21424de47ec63b3b0 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("******************************************************");
     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)
   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> 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 *********");
 
 
   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 =
 
       /* 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).
 
       /* 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
         && 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())
 
         /* 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 291d98ec4f255723337022bd35a72043cc836c06..781c2ba1434d748deed0dbdc5dbb24aad71303b5 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_;
   /** 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
 };
 
 #endif

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index e5613cd6bf453ea1b7214fd1dfafd66b94bfb639..e3688e292f3d1dbdc7b07e1b4d3ad91e6e64a8c9 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;
 {
   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;
   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 3cbfce31bf9bfe912c08c5cc080663cd3dfca899..128722ba60e1150b264ba467c9f0abbdaebd9b80 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;
   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 b51d39adae89d61565177cae39941a46a251613c..e59dd97b95db725d93263f621d2a68d14530f232 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();
 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);
 }
   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 =
 
     /* 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();
 
     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
     }
 
     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())
 
       /* 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 =
   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");
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");

diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index a9662be45bcd6faa198823725eb076cfb008677e..71b5f67d92c571c045d571f70ba71d9065b62c9c 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_;
   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 746a0f115d4b556b1a1a0e16c3f91a4cbf3980af..6d0e87e7cc8a3630be082116d877662168bfbda4 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.
  */
  * \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(
 {
   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->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;
 }
 
   this->other_num = -1;
 }
 


@@ -76,10 +76,11 @@ void VisitedStates::prune()
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
 /**
  * \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_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);
   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 364c8bfa52710cd2dd8b3df1ca6db4b0f0140a18..13691af2e3ed677be48c4cf65d77539fd6305a96 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
 
   int num = 0;
   int other_num = 0; // dot_output for
 

-  VisitedState();
+  VisitedState(unsigned long state_number);

   ~VisitedState();
 };
 
   ~VisitedState();
 };
 


@@ -31,7 +31,7 @@ class XBT_PRIVATE VisitedStates {
   std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
 public:
   void clear() { states_.clear(); }
   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();
 };
 private:
   void prune();
 };

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 83083888f1fd9280670bce015d2b065d30ea2589..ae5e000deb0418d20631dba349921320fea5ed96 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;
 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;
 
   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 8f675cf61d561957c1c3ac431a735a261053ae85..50df4a3f11950c002db40e9183e9aa4c0e7f668c 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
  */
 /**
  * \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());
 {
   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 */
   /* 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);
     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 43554bffd0fe0121def79099962f06c75bd00c32..599b0cb785e8a59ab7d05a55eb2530d49eac90f3 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
 XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state);
 
 #endif