X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/00e79d1291f14583564ed0eba2d5e56ee30bf7d3..a88428006c545383c30052e5606b3f8e895bd9d8:/src/mc/explo/DFSExplorer.cpp

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 386c43c097..05b607b850 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
@@ -80,7 +81,7 @@ 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_, visited_states_count_,
            Transition::get_replayed_transitions());
@@ -144,14 +145,12 @@ void DFSExplorer::run()
       continue;
     }
 
-    if (_sg_mc_sleep_set) {
-	XBT_VERB("Sleep set actually containing:");
-	for (auto & [aid, transition] : state->get_sleep_set()) {
-   
-	    XBT_VERB("  <%ld,%s>", aid, transition.to_string().c_str());
-      
-	}
+    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);
     on_transition_execute_signal(state->get_transition(), get_remote_app());
@@ -167,9 +166,9 @@ void DFSExplorer::run()
     /* 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); 
+      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());
 
     on_state_creation_signal(next_state.get(), get_remote_app());
 
@@ -225,10 +224,11 @@ void DFSExplorer::backtrack()
   bool found_backtracking_point = false;
   while (not stack_.empty() && not found_backtracking_point) {
     std::unique_ptr<State> state = std::move(stack_.back());
-    
+
     stack_.pop_back();
-    
-    XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+
+    XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
+              state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
     state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
 
     if (reduction_mode_ == ReductionMode::dpor) {
@@ -244,15 +244,17 @@ void DFSExplorer::backtrack()
           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 (prev_state->is_actor_enabled(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_enabled_todo();
-	  }
+          if (prev_state->is_actor_enabled(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_enabled_todo();
+          }
           break;
         } else {
           XBT_VERB("INDEPENDENT Transitions:");