Document more changes, and update the Release Notes

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

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 9ef0daf..57b2202 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2016-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -13,6 +13,7 @@
 
 #include "src/xbt/mmalloc/mmprivate.h"
 #include "xbt/log.h"
+#include "xbt/string.hpp"
 #include "xbt/sysdep.h"
 
 #include <cassert>
@@ -49,7 +50,9 @@ void DFSExplorer::check_non_termination(const State* current_state)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      XBT_INFO("Path = %s", get_record_trace().to_string().c_str());
+      XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+               "--cfg=model-check/replay:'%s'",
+               get_record_trace().to_string().c_str());
       log_state();
 
       throw TerminationError();
@@ -95,7 +98,7 @@ void DFSExplorer::run()
     State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth=%zu (state:%ld; %zu interleaves)", stack_.size(), state->get_num(),
+    XBT_DEBUG("Exploration depth=%zu (state:#%ld; %zu interleaves todo)", stack_.size(), state->get_num(),
               state->count_todo());
 
     mc_model_checker->inc_visited_states();
@@ -123,10 +126,10 @@ void DFSExplorer::run()
     }
 
     // Search for the next transition
-    int next = state->next_transition();
+    aid_t next = state->next_transition();
 
     if (next < 0) { // If there is no more transition in the current state, backtrack.
-      XBT_DEBUG("There remains %d actors, but none to interleave (depth %zu).", state->get_actor_count(),
+      XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
                 stack_.size() + 1);
 
       if (state->get_actor_count() == 0) {
@@ -171,7 +174,6 @@ void DFSExplorer::run()
 
       mc_model_checker->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
@@ -284,7 +286,7 @@ DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Explo
   XBT_DEBUG("**************************************************");
 
   /* Get an enabled actor and insert it in the interleave set of the initial state */
-  XBT_DEBUG("Initial state. %d actors to consider", initial_state->get_actor_count());
+  XBT_DEBUG("Initial state. %lu actors to consider", initial_state->get_actor_count());
   for (auto const& [aid, _] : initial_state->get_actors_list()) {
     if (initial_state->is_actor_enabled(aid)) {
       initial_state->mark_todo(aid);