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 03122f3..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();