Forgot to add c++17g to the "ignore" list.

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

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index a98f32dc276b1d3159880d8d683646586592f04b..7bd96aa7063b8b0e5dd7febb4cc1436090b56aa8 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -80,10 +80,11 @@ std::vector<std::string> DFSExplorer::get_textual_trace() // override
 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 "
+  XBT_INFO("DFS exploration ended. %ld unique states visited; %lu 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) {
@@ -118,7 +119,7 @@ void DFSExplorer::run()
     // Backtrack if we are revisiting a state we saw previously
     if (visited_state_ != nullptr) {
       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_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
 
       visited_state_ = nullptr;
       this->backtrack();
@@ -178,26 +179,25 @@ 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->get_num(), next_state.get());
+      visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
 
     /* If this is a new state (or if we don't care about state-equality reduction) */
     if (visited_state_ == nullptr) {
       /* Get an enabled process and insert it in the interleave set of the next state */
       for (auto const& [aid, _] : next_state->get_actors_list()) {
-        if (next_state->is_actor_enabled(aid) and not next_state->is_done(aid)) {
+        if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) {
           next_state->mark_todo(aid);
           if (reduction_mode_ == ReductionMode::dpor)
             break; // With DPOR, we take the first enabled transition
         }
       }
 
-      mc_model_checker->dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
-                                   state->get_transition()->dot_string().c_str());
+      dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), next_state->get_num(),
+                 state->get_transition()->dot_string().c_str());
     } else
-      mc_model_checker->dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
-                                   visited_state_->original_num == -1 ? visited_state_->num
-                                                                      : visited_state_->original_num,
-                                   state->get_transition()->dot_string().c_str());
+      dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(),
+                 visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_,
+                 state->get_transition()->dot_string().c_str());
 
     stack_.push_back(std::move(next_state));
   }
@@ -245,13 +245,13 @@ void DFSExplorer::backtrack()
           XBT_VERB("  %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
 
          if (prev_state->is_actor_enabled(issuer_id)){
-             if (not prev_state->is_done(issuer_id))
+             if (not prev_state->is_actor_done(issuer_id))
                  prev_state->mark_todo(issuer_id);
              else
                  XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
          } else {
              XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled transition as todo", issuer_id);
-             prev_state->mark_all_todo();
+             prev_state->mark_all_enabled_todo();
          }
           break;
         } else {
@@ -292,8 +292,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
 }