[sonar] Don't mix public and private members (mc::State).

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index ad9a135..873154c 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -44,9 +44,9 @@ std::unique_ptr<simgrid::mc::VisitedState>
 VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snapshots)
 {
   auto new_state             = std::make_unique<simgrid::mc::VisitedState>(state_number);
-  graph_state->system_state_ = new_state->system_state;
+  graph_state->set_system_state(new_state->system_state);
   XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(),
-            new_state->num, graph_state->num_);
+            new_state->num, graph_state->get_num());
 
   auto range = boost::range::equal_range(states_, new_state.get(), Api::get().compare_pair());
 

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 377453d..a9aaba9 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -101,7 +101,7 @@ void Api::mc_exit(int status) const
   mc_model_checker->exit(status);
 }
 
-void Api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const
+void Api::restore_state(simgrid::mc::Snapshot* system_state) const
 {
   system_state->restore(&mc_model_checker->get_remote_process());
 }

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 39d658e..19daf85 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -69,7 +69,7 @@ public:
   XBT_ATTRIB_NORETURN void mc_exit(int status) const;
 
   // STATE APIs
-  void restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const;
+  void restore_state(Snapshot* system_state) const;
 
   // SNAPSHOT APIs
   bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index bc5f7a0..dd243f8 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -20,9 +20,6 @@ class XBT_PRIVATE State : public xbt::Extendable<State> {
   /* Outgoing transition: what was the last transition that we took to leave this state? */
   std::unique_ptr<Transition> transition_;
 
-public:
-  explicit State();
-
   /** Sequential state number (used for debugging) */
   long num_ = 0;
 
@@ -30,7 +27,10 @@ public:
   std::vector<ActorState> actor_states_;
 
   /** Snapshot of system state (if needed) */
-  std::shared_ptr<simgrid::mc::Snapshot> system_state_;
+  std::shared_ptr<Snapshot> system_state_;
+
+public:
+  explicit State();
 
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   int next_transition() const;
@@ -38,11 +38,16 @@ public:
   /* Explore a new path; the parameter must be the result of a previous call to next_transition() */
   void execute_next(int next);
 
+  long get_num() const { return num_; }
   std::size_t count_todo() const;
   void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); }
+  bool is_done(aid_t actor) const { return this->actor_states_[actor].is_done(); }
   Transition* get_transition() const;
   void set_transition(Transition* t) { transition_.reset(t); }
 
+  Snapshot* get_system_state() const { return system_state_.get(); }
+  void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
+
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }
 };

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 286c3f7..5e41cfa 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -42,8 +42,8 @@ xbt::signal<void()> DFSExplorer::on_log_state_signal;
 void DFSExplorer::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 %ld -> state %ld", (*state)->num_, current_state->num_);
+    if (Api::get().snapshot_equal((*state)->get_system_state(), current_state->get_system_state())) {
+      XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num());
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
       XBT_INFO("******************************************");
@@ -96,7 +96,8 @@ void DFSExplorer::run()
     State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->num_, state->count_todo());
+    XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->get_num(),
+              state->count_todo());
 
     Api::get().mc_inc_visited_states();
 
@@ -132,7 +133,7 @@ void DFSExplorer::run()
       if (mc_model_checker->get_remote_process().actors().empty()) {
         mc_model_checker->finalize_app();
         XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
-                 state->num_, stack_.size());
+                 state->get_num(), stack_.size());
       }
       this->backtrack();
       continue;
@@ -145,7 +146,7 @@ void DFSExplorer::run()
     // If there are processes to interleave and the maximum depth has not been
     // reached then perform one step of the exploration algorithm.
     XBT_VERB("Execute %ld: %.60s (stack depth: %zu, state: %ld, %zu interleaves)", state->get_transition()->aid_,
-             state->get_transition()->to_string().c_str(), stack_.size(), state->num_, state->count_todo());
+             state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
 
     std::string req_str;
     if (dot_output != nullptr)
@@ -160,7 +161,7 @@ void DFSExplorer::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(next_state->num_, next_state.get(), true);
+      visited_state_ = visited_states_.addVisitedState(next_state->get_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) {
@@ -176,10 +177,11 @@ void DFSExplorer::run()
       }
 
       if (dot_output != nullptr)
-        std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
+        std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
+                     req_str.c_str());
 
     } else if (dot_output != nullptr)
-      std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->num_,
+      std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
                    visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
                    req_str.c_str());
 
@@ -216,32 +218,32 @@ void DFSExplorer::backtrack()
           break;
         } else if (prev_state->get_transition()->depends(state->get_transition())) {
           XBT_VERB("Dependent Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_);
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_);
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
 
-          if (not prev_state->actor_states_[issuer_id].is_done())
+          if (not prev_state->is_done(issuer_id))
             prev_state->mark_todo(issuer_id);
           else
             XBT_DEBUG("Actor %ld is in done set", issuer_id);
           break;
         } else {
           XBT_VERB("INDEPENDENT Transitions:");
-          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_);
-          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_);
+          XBT_VERB("  %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
+          XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
         }
       }
     }
 
     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 %ld at depth %zu", state->num_, stack_.size() + 1);
+      XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->get_num(), stack_.size() + 1);
       stack_.push_back(
           std::move(state)); // Put it back on the stack from which it was removed earlier in this while loop
       this->restore_state();
-      XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size());
+      XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->get_num(), stack_.size());
       break;
     } else {
-      XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1);
+      XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
     }
   }
 }
@@ -250,8 +252,8 @@ void DFSExplorer::restore_state()
 {
   /* If asked to rollback on a state that has a snapshot, restore it */
   State* last_state = stack_.back().get();
-  if (last_state->system_state_) {
-    Api::get().restore_state(last_state->system_state_);
+  if (auto* system_state = last_state->get_system_state()) {
+    Api::get().restore_state(system_state);
     on_restore_system_state_signal(last_state);
     return;
   }

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index b8de82a..edb3cf5 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -25,8 +25,8 @@ VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state,
     : num(pair_num), automaton_state(automaton_state)
 {
   this->graph_state = std::move(graph_state);
-  if (this->graph_state->system_state_ == nullptr)
-    this->graph_state->system_state_ = std::make_shared<Snapshot>(pair_num);
+  if (not this->graph_state->get_system_state())
+    this->graph_state->set_system_state(std::make_shared<Snapshot>(pair_num));
   this->heap_bytes_used     = Api::get().get_remote_heap_bytes();
   this->actors_count        = Api::get().get_actors().size();
   this->other_num           = -1;
@@ -71,8 +71,8 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 ||
           *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
-          not Api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
-                                        new_pair->graph_state->system_state_.get()))
+          not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(),
+                                        new_pair->graph_state->get_system_state()))
         continue;
       XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
       exploration_stack_.pop_back();
@@ -102,8 +102,8 @@ void LivenessChecker::replay()
   /* Intermediate backtracking */
   if (_sg_mc_checkpoint > 0) {
     const Pair* pair = exploration_stack_.back().get();
-    if (pair->graph_state->system_state_) {
-      Api::get().restore_state(pair->graph_state->system_state_);
+    if (auto* system_state = pair->graph_state->get_system_state()) {
+      Api::get().restore_state(system_state);
       return;
     }
   }
@@ -148,8 +148,8 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     const VisitedPair* pair_test = i->get();
     if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
-        not Api::get().snapshot_equal(pair_test->graph_state->system_state_.get(),
-                                      visited_pair->graph_state->system_state_.get()))
+        not Api::get().snapshot_equal(pair_test->graph_state->get_system_state(),
+                                      visited_pair->graph_state->get_system_state()))
       continue;
     if (pair_test->other_num == -1)
       visited_pair->other_num = pair_test->num;