Move state stack management to member on UnfoldingChecker

[simgrid.git] / src / mc / explo / DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index d2a9b1f6aaf1395458f2d85689f8f265c84237ed..93848b01440cc0bf966e1cf74b32a943695cfd7a 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -10,7 +10,7 @@
 #include "src/mc/mc_record.hpp"
 #include "src/mc/transition/Transition.hpp"
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
 #include "src/mc/VisitedState.hpp"
 #endif
 
@@ -44,7 +44,7 @@ xbt::signal<void(RemoteApp&)> DFSExplorer::on_log_state_signal;
 
 void DFSExplorer::check_non_termination(const State* current_state)
 {
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
   for (auto const& state : stack_) {
     if (state->get_system_state()->equals_to(*current_state->get_system_state(),
                                              *get_remote_app().get_remote_process_memory())) {
@@ -139,7 +139,7 @@ void DFSExplorer::run()
       continue;
     }
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
     // Backtrack if we are revisiting a state we saw previously while applying state-equality reduction
     if (visited_state_ != nullptr) {
       XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.",
@@ -218,7 +218,7 @@ void DFSExplorer::run()
           if (prev_state->is_actor_enabled(issuer_id)) {
             if (not prev_state->is_actor_done(issuer_id)) {
               prev_state->consider_one(issuer_id);
-              opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+              opened_states_.emplace(tmp_stack.back());
             } else
               XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
           } else {
@@ -227,7 +227,7 @@ void DFSExplorer::run()
                       issuer_id);
             // If we ended up marking at least a transition, explore it at some point
             if (prev_state->consider_all() > 0)
-              opened_states_.push(std::shared_ptr<State>(tmp_stack.back()));
+              opened_states_.emplace(tmp_stack.back());
           }
           break;
         } else {
@@ -242,12 +242,12 @@ void DFSExplorer::run()
     // Before leaving that state, if the transition we just took can be taken multiple times, we
     // need to give it to the opened states
     if (stack_.back()->count_todo_multiples() > 0)
-      opened_states_.push(std::shared_ptr<State>(stack_.back()));
+      opened_states_.emplace(stack_.back());
 
     if (_sg_mc_termination)
       this->check_non_termination(next_state.get());
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
     /* 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->get_num(), next_state.get(), get_remote_app());
@@ -266,7 +266,7 @@ void DFSExplorer::run()
 
       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(),
                  state->get_transition()->dot_string().c_str());
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
     } else {
       dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
                  visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
@@ -292,8 +292,8 @@ void DFSExplorer::backtrack()
     return;
   }
 
-  std::shared_ptr<State> backtracking_point = opened_states_.top(); // Take the point with smallest distance
-  opened_states_.pop();
+  // Take the point with smallest distance
+  auto backtracking_point = opened_states_.extract(begin(opened_states_)).value();
 
   // if the smallest distance corresponded to no enable actor, remove this and let the
   // exploration ask again for a backtrack
@@ -307,7 +307,7 @@ void DFSExplorer::backtrack()
   backtrack_count_++;
   XBT_DEBUG("Backtracking to state#%ld", backtracking_point->get_num());
 
-#if SIMGRID_HAVE_MC
+#if SIMGRID_HAVE_STATEFUL_MC
   /* If asked to rollback on a state that has a snapshot, restore it */
   if (const auto* system_state = backtracking_point->get_system_state()) {
     system_state->restore(*get_remote_app().get_remote_process_memory());
@@ -361,7 +361,7 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool ne
     stack_.back()->consider_all();
   }
   if (stack_.back()->count_todo_multiples() > 1)
-    opened_states_.push(std::shared_ptr<State>(stack_.back()));
+    opened_states_.emplace(stack_.back());
 }
 
 Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)