Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Default is not to use sleep-set to agree with existing tests
[simgrid.git] / src / mc / ModelChecker.cpp
index 17e2bce..616e838 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2008-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. */
@@ -156,7 +156,9 @@ static void MC_report_crash(Exploration* explorer, int status)
     XBT_INFO("Counter-example execution trace:");
     for (auto const& s : explorer->get_textual_trace())
       XBT_INFO("  %s", s.c_str());
-    XBT_INFO("Path = %s", explorer->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'",
+             explorer->get_record_trace().to_string().c_str());
     explorer->log_state();
     if (xbt_log_no_loc) {
       XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
@@ -241,7 +243,9 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      XBT_INFO("Path = %s", get_exploration()->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_exploration()->get_record_trace().to_string().c_str());
       exploration_->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);