Move the stats of visited_states count from ModelChecker to DFSExplorer where it...

diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp
index d7a7cc3..d32bd26 100644 (file)
--- a/src/mc/ModelChecker.hpp
+++ b/src/mc/ModelChecker.hpp
@@ -24,8 +24,6 @@ class ModelChecker {
   std::unique_ptr<RemoteProcess> remote_process_;
   Exploration* exploration_ = nullptr;
 
-  unsigned long visited_states_ = 0;
-
 public:
   ModelChecker(ModelChecker const&) = delete;
   ModelChecker& operator=(ModelChecker const&) = delete;
@@ -51,9 +49,6 @@ public:
   Exploration* get_exploration() const { return exploration_; }
   void set_exploration(Exploration* exploration) { exploration_ = exploration; }
 
-  unsigned long get_visited_states() const { return visited_states_; }
-  void inc_visited_states() { visited_states_++; }
-
 private:
   void setup_ignore();
   bool handle_message(const char* buffer, ssize_t size);

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 76c5688..4c3657f 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -82,8 +82,9 @@ void DFSExplorer::log_state() // override
   on_log_state_signal(get_remote_app());
   XBT_INFO("DFS exploration ended. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states "
            "visited overall)",
-           State::get_expanded_states(), backtrack_count_, mc_model_checker->get_visited_states(),
+           State::get_expanded_states(), backtrack_count_, visited_states_count_,
            Transition::get_replayed_transitions());
+  Exploration::log_state();
 }
 
 void DFSExplorer::run()
@@ -101,7 +102,7 @@ void DFSExplorer::run()
     XBT_DEBUG("Exploration depth=%zu (state:#%ld; %zu interleaves todo)", stack_.size(), state->get_num(),
               state->count_todo());
 
-    mc_model_checker->inc_visited_states();
+    visited_states_count_++;
 
     // Backtrack if we reached the maximum depth
     if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
@@ -292,8 +293,7 @@ void DFSExplorer::backtrack()
         break;
       state->get_transition()->replay();
       on_transition_replay_signal(state->get_transition(), get_remote_app());
-      /* Update statistics */
-      mc_model_checker->inc_visited_states();
+      visited_states_count_++;
     }
   } // If no backtracing point, then the stack is empty and the exploration is over
 }

diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp
index 0a0d51e..8d63ca4 100644 (file)
--- a/src/mc/explo/DFSExplorer.hpp
+++ b/src/mc/explo/DFSExplorer.hpp
@@ -20,7 +20,8 @@ class XBT_PRIVATE DFSExplorer : public Exploration {
   XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor);
 
   ReductionMode reduction_mode_;
-  long backtrack_count_        = 0;
+  unsigned long backtrack_count_      = 0; // for statistics
+  unsigned long visited_states_count_ = 0; // for statistics
 
   static xbt::signal<void(RemoteApp&)> on_exploration_start_signal;
   static xbt::signal<void(RemoteApp&)> on_backtracking_signal;