From d872d0c0ec6694fee02a2ede409ad22fcab9258c Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 2 Mar 2023 23:59:14 +0100 Subject: [PATCH] Move the stats of visited_states count from ModelChecker to DFSExplorer where it belongs --- src/mc/ModelChecker.hpp | 5 ----- src/mc/explo/DFSExplorer.cpp | 8 ++++---- src/mc/explo/DFSExplorer.hpp | 3 ++- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index d7a7cc307f..d32bd262ee 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -24,8 +24,6 @@ class ModelChecker { std::unique_ptr 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 76c568804d..4c3657ffa6 100644 --- 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 0a0d51e53d..8d63ca4e23 100644 --- 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 on_exploration_start_signal; static xbt::signal on_backtracking_signal; -- 2.20.1