Unify the way we count expended states between checkers

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 3702c94..436ab81 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -47,7 +47,7 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
 {
   auto new_state             = std::make_unique<simgrid::mc::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(),
+  XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(),
             new_state->num, graph_state->num_);
 
   auto range =
@@ -68,24 +68,22 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
           new_state->original_num = old_state->original_num;
 
         if (dot_output == nullptr)
-          XBT_DEBUG("State %d already visited ! (equal to state %d)",
-                    new_state->num, old_state->num);
+          XBT_DEBUG("State %ld already visited ! (equal to state %ld)", new_state->num, old_state->num);
         else
-          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))",
-                    new_state->num, old_state->num, new_state->original_num);
+          XBT_DEBUG("State %ld already visited ! (equal to state %ld (state %ld in dot_output))", new_state->num,
+                    old_state->num, new_state->original_num);
 
         /* Replace the old state with the new one (with a bigger num)
            (when the max number of visited states is reached,  the oldest
            one is removed according to its number (= with the min number) */
-        XBT_DEBUG("Replace visited state %d with the new visited state %d",
-          old_state->num, new_state->num);
+        XBT_DEBUG("Replace visited state %ld with the new visited state %ld", old_state->num, new_state->num);
 
         visited_state = std::move(new_state);
         return old_state;
       }
     }
 
-  XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) states_.size());
+  XBT_DEBUG("Insert new visited state %ld (total : %lu)", new_state->num, (unsigned long)states_.size());
   states_.insert(range.first, std::move(new_state));
   this->prune();
   return nullptr;

diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
index 4e13155..4fe702f 100644 (file)
--- a/src/mc/VisitedState.hpp
+++ b/src/mc/VisitedState.hpp
@@ -20,8 +20,8 @@ public:
   std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
   std::size_t heap_bytes_used = 0;
   int actors_count            = 0;
-  int num          = 0; // unique id of that state in the storage of all stored IDs
-  int original_num = -1; // num field of the VisitedState to which I was declared equal to (used for dot_output)
+  long num                                            = 0; // unique id of that state in the storage of all stored IDs
+  long original_num = -1; // num field of the VisitedState to which I was declared equal to (used for dot_output)
 
   explicit VisitedState(unsigned long state_number);
 };

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 4d99e55..47b230a 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -290,7 +290,7 @@ void CommunicationDeterminismChecker::log_state() // override
       XBT_INFO("%s", this->send_diff);
     }
   }
-  XBT_INFO("Expanded states = %lu", expanded_states_count_);
+  XBT_INFO("Expanded states = %ld", State::get_expanded_states());
   XBT_INFO("Visited states = %lu", api::get().mc_get_visited_states());
   XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
   XBT_INFO("Send-deterministic : %s", this->send_deterministic ? "Yes" : "No");
@@ -305,8 +305,7 @@ void CommunicationDeterminismChecker::prepare()
   initial_communications_pattern.resize(maxpid);
   incomplete_communications_pattern.resize(maxpid);
 
-  ++expanded_states_count_;
-  auto initial_state = std::make_unique<State>(expanded_states_count_);
+  auto initial_state = std::make_unique<State>();
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -412,7 +411,7 @@ void CommunicationDeterminismChecker::real_run()
     State* cur_state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth = %zu (state = %d, interleaved processes = %zu)", stack_.size(), cur_state->num_,
+    XBT_DEBUG("Exploration depth = %zu (state = %ld, interleaved processes = %zu)", stack_.size(), cur_state->num_,
               cur_state->count_todo());
 
     /* Update statistics */
@@ -443,8 +442,7 @@ void CommunicationDeterminismChecker::real_run()
       handle_comm_pattern(call, req, req_num, 0);
 
       /* Create the new expanded state */
-      ++expanded_states_count_;
-      auto next_state = std::make_unique<State>(expanded_states_count_);
+      auto next_state = std::make_unique<State>();
 
       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared
@@ -452,7 +450,7 @@ void CommunicationDeterminismChecker::real_run()
       bool compare_snapshots = this->initial_communications_pattern_done && all_communications_are_finished();
 
       if (_sg_mc_max_visited_states != 0)
-        visited_state = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), compare_snapshots);
+        visited_state = visited_states_.addVisitedState(next_state->num_, next_state.get(), compare_snapshots);
       else
         visited_state = nullptr;
 
@@ -465,10 +463,10 @@ void CommunicationDeterminismChecker::real_run()
         }
 
         if (dot_output != nullptr)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str());
+          fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str());
 
       } else if (dot_output != nullptr)
-        fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num_,
+        fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_,
                 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
 
       stack_.push_back(std::move(next_state));
@@ -476,7 +474,7 @@ void CommunicationDeterminismChecker::real_run()
       if (stack_.size() > (std::size_t)_sg_mc_max_depth)
         XBT_WARN("/!\\ Max depth reached! /!\\ ");
       else if (visited_state != nullptr)
-        XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
+        XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
                   visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
       else
         XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size());
@@ -484,7 +482,7 @@ void CommunicationDeterminismChecker::real_run()
       this->initial_communications_pattern_done = true;
 
       /* Trash the current state, no longer needed */
-      XBT_DEBUG("Delete state %d at depth %zu", cur_state->num_, stack_.size());
+      XBT_DEBUG("Delete state %ld at depth %zu", cur_state->num_, stack_.size());
       stack_.pop_back();
 
       visited_state = nullptr;
@@ -496,16 +494,16 @@ void CommunicationDeterminismChecker::real_run()
         stack_.pop_back();
         if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
+          XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->num_, stack_.size() + 1);
           stack_.push_back(std::move(state));
 
           this->restoreState();
 
-          XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
+          XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size());
 
           break;
         } else {
-          XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
+          XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1);
         }
       }
     }

diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp
index 7610407..0a496ed 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.hpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.hpp
@@ -41,7 +41,6 @@ private:
   /** Stack representing the position in the exploration graph */
   std::list<std::unique_ptr<State>> stack_;
   VisitedStates visited_states_;
-  unsigned long expanded_states_count_ = 0;
 
   bool initial_communications_pattern_done = false;
   bool recv_deterministic                  = true;

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 06d3efd..c4a214a 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -226,10 +226,9 @@ std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt
                                                    std::shared_ptr<const std::vector<int>> propositions)
 {
   ++expanded_pairs_count_;
-  ++expanded_states_count_;
   auto next_pair                  = std::make_shared<Pair>(expanded_pairs_count_);
   next_pair->automaton_state      = state;
-  next_pair->graph_state          = std::make_shared<State>(expanded_states_count_);
+  next_pair->graph_state          = std::make_shared<State>();
   next_pair->atomic_propositions  = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;

diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp
index ec1969e..11388df 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/checker/LivenessChecker.hpp
@@ -75,7 +75,6 @@ private:
   std::list<std::shared_ptr<VisitedPair>> visited_pairs_;
   unsigned long visited_pairs_count_   = 0;
   unsigned long expanded_pairs_count_  = 0;
-  unsigned long expanded_states_count_ = 0;
   int previous_pair_                   = 0;
   std::string previous_request_;
 };

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index f91565d..72192fa 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -34,7 +34,7 @@ void SafetyChecker::check_non_termination(const State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
     if (api::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
-      XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
+      XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->num_, current_state->num_);
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
       XBT_INFO("******************************************");
@@ -66,7 +66,7 @@ std::vector<std::string> SafetyChecker::get_textual_trace() // override
 
 void SafetyChecker::log_state() // override
 {
-  XBT_INFO("Expanded states = %lu", expanded_states_count_);
+  XBT_INFO("Expanded states = %ld", State::get_expanded_states());
   XBT_INFO("Visited states = %lu", api::get().mc_get_visited_states());
   XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions());
 }
@@ -82,7 +82,7 @@ void SafetyChecker::run()
     State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num_,
+    XBT_VERB("Exploration depth=%zu (state=%p, num %ld)(%zu interleave)", stack_.size(), state, state->num_,
              state->count_todo());
 
     api::get().mc_inc_visited_states();
@@ -101,7 +101,7 @@ void SafetyChecker::run()
 
     // Backtrack if we are revisiting a state we saw previously
     if (visited_state_ != nullptr) {
-      XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
+      XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
                 visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num);
 
       visited_state_ = nullptr;
@@ -136,8 +136,7 @@ void SafetyChecker::run()
           api::get().request_get_dot_output(state->get_transition()->aid_, state->get_transition()->times_considered_);
 
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
-    ++expanded_states_count_;
-    auto next_state = std::make_unique<State>(expanded_states_count_);
+    auto next_state              = std::make_unique<State>();
     next_state->remote_observer_ = remote_observer;
 
     if (_sg_mc_termination)
@@ -145,7 +144,7 @@ void SafetyChecker::run()
 
     /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
     if (_sg_mc_max_visited_states > 0)
-      visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true);
+      visited_state_ = visited_states_.addVisitedState(next_state->num_, next_state.get(), true);
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {
@@ -161,10 +160,10 @@ void SafetyChecker::run()
       }
 
       if (dot_output != nullptr)
-        std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
+        std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
 
     } else if (dot_output != nullptr)
-      std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_,
+      std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_,
                    visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
                    req_str.c_str());
 
@@ -200,8 +199,8 @@ void SafetyChecker::backtrack()
         } else if (api::get().requests_are_dependent(prev_state->remote_observer_, state->remote_observer_)) {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("Dependent Transitions:");
-            XBT_DEBUG("  %s (state=%d)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_cstring(), state->num_);
+            XBT_DEBUG("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+            XBT_DEBUG("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
           }
 
           if (not prev_state->actor_states_[issuer_id].is_done())
@@ -212,8 +211,8 @@ void SafetyChecker::backtrack()
         } else {
           if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
             XBT_DEBUG("INDEPENDENT Transitions:");
-            XBT_DEBUG("  %s (state=%d)", prev_state->get_transition()->to_cstring(), prev_state->num_);
-            XBT_DEBUG("  %s (state=%d)", state->get_transition()->to_cstring(), state->num_);
+            XBT_DEBUG("  %s (state=%ld)", prev_state->get_transition()->to_cstring(), prev_state->num_);
+            XBT_DEBUG("  %s (state=%ld)", state->get_transition()->to_cstring(), state->num_);
           }
         }
       }
@@ -221,13 +220,13 @@ void SafetyChecker::backtrack()
 
     if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
       /* We found a back-tracking point, let's loop */
-      XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
+      XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->num_, stack_.size() + 1);
       stack_.push_back(std::move(state));
       this->restore_state();
-      XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
+      XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size());
       break;
     } else {
-      XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
+      XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1);
     }
   }
 }
@@ -272,8 +271,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session)
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  ++expanded_states_count_;
-  auto initial_state = std::make_unique<State>(expanded_states_count_);
+  auto initial_state = std::make_unique<State>();
 
   XBT_DEBUG("**************************************************");
 

diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp
index f554b06..9a934a8 100644 (file)
--- a/src/mc/checker/SafetyChecker.hpp
+++ b/src/mc/checker/SafetyChecker.hpp
@@ -38,7 +38,6 @@ private:
   std::list<std::unique_ptr<State>> stack_;
   VisitedStates visited_states_;
   std::unique_ptr<VisitedState> visited_state_;
-  unsigned long expanded_states_count_ = 0;
 };
 
 } // namespace mc

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index d5a082d..f0fbc1c 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -18,12 +18,14 @@ using api = simgrid::mc::Api;
 namespace simgrid {
 namespace mc {
 
-State::State(unsigned long state_number) : num_(state_number)
+long State::expended_states_ = 0;
+
+State::State() : num_(++expended_states_)
 {
   const unsigned long maxpid = api::get().get_maxpid();
   actor_states_.resize(maxpid);
   /* Stateful model checking */
-  if ((_sg_mc_checkpoint > 0 && (state_number % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
+  if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
     auto snapshot_ptr = api::get().take_snapshot(num_);
     system_state_ = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {

diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp
index 60e9e10..858f00b 100644 (file)
--- a/src/mc/mc_state.hpp
+++ b/src/mc/mc_state.hpp
@@ -15,11 +15,16 @@ namespace mc {
 
 /* A node in the exploration graph (kind-of) */
 class XBT_PRIVATE State {
+  static long expended_states_; /* Count total amount of states, for stats */
+
+  /* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */
   Transition transition_;
 
 public:
+  explicit State();
+
   /** Sequential state number (used for debugging) */
-  int num_ = 0;
+  long num_ = 0;
 
   /** State's exploration status by process */
   std::vector<ActorState> actor_states_;
@@ -37,7 +42,6 @@ public:
   std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
   std::vector<unsigned> communication_indices_;
 
-  explicit State(unsigned long state_number);
 
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   int next_transition() const;
@@ -49,6 +53,9 @@ public:
   void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); }
   Transition* get_transition() const;
 
+  /* Returns the total amount of states created so far (for statistics) */
+  static long get_expanded_states() { return expended_states_; }
+
 private:
   void copy_incomplete_comm_pattern();
   void copy_index_comm_pattern();