X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/0f76f48403c7bbf6e6e26df305bed9b583504057..239cd16f4e95031d3a106e487c1485726069f1d7:/src/mc/explo/DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 936a2a56e5..84753958e4 100644
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -41,9 +41,9 @@ xbt::signal<void(RemoteApp&)> DFSExplorer::on_log_state_signal;
 
 void DFSExplorer::check_non_termination(const State* current_state)
 {
-  for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
-    if (*(*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());
+  for (auto const& state : stack_) {
+    if (*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("******************************************");
@@ -57,6 +57,7 @@ void DFSExplorer::check_non_termination(const State* current_state)
 
       throw TerminationError();
     }
+  }
 }
 
 RecordTrace DFSExplorer::get_record_trace() // override
@@ -116,7 +117,7 @@ void DFSExplorer::run()
       continue;
     }
 
-    // Backtrack if we are revisiting a state we saw previously
+    // 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.",
                 visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_);
@@ -134,7 +135,7 @@ void DFSExplorer::run()
                 stack_.size() + 1);
       
       if (state->get_actor_count() == 0) {
-        mc_model_checker->finalize_app();
+        get_remote_app().finalize_app();
         XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
                  state->get_num(), stack_.size());
 
@@ -144,14 +145,14 @@ void DFSExplorer::run()
       continue;
     }
 
-    if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(XBT_LOG_DEFAULT_CATEGORY, xbt_log_priority_verbose)) {
+    if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) {
       XBT_VERB("Sleep set actually containing:");
       for (auto& [aid, transition] : state->get_sleep_set())
         XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
     }
 
     /* Actually answer the request: let's execute the selected request (MCed does one step) */
-    state->execute_next(next);
+    state->execute_next(next, get_remote_app());
     on_transition_execute_signal(state->get_transition(), get_remote_app());
 
     // If there are processes to interleave and the maximum depth has not been
@@ -162,12 +163,7 @@ void DFSExplorer::run()
     /* Create the new expanded state (copy the state of MCed into our MCer data) */
     std::unique_ptr<State> next_state;
 
-    /* If we want sleep set reduction, pass the old state to the new state so it can
-     * both copy the sleep set and eventually removes things from it locally */
-    if (_sg_mc_sleep_set)
-      next_state = std::make_unique<State>(get_remote_app(), state);
-    else
-      next_state = std::make_unique<State>(get_remote_app());
+    next_state = std::make_unique<State>(get_remote_app(), state);
 
     on_state_creation_signal(next_state.get(), get_remote_app());
 
@@ -278,7 +274,7 @@ void DFSExplorer::backtrack()
     /* If asked to rollback on a state that has a snapshot, restore it */
     State* last_state = stack_.back().get();
     if (const auto* system_state = last_state->get_system_state()) {
-      system_state->restore(&get_remote_app().get_remote_process());
+      system_state->restore(get_remote_app().get_remote_process_memory());
       on_restore_system_state_signal(last_state, get_remote_app());
       return;
     }