MC: tell the user about how to use the replay path in case of problem

diff --git a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
index bd135cf..97ec9d5 100644 (file)
--- a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
+++ b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
@@ -31,5 +31,5 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1 ${platfdir:=.
 > [  0.000000] (0:maestro@)   1: iRecv(mbox=0)
 > [  0.000000] (0:maestro@)   3: iSend(mbox=0)
 > [  0.000000] (0:maestro@)   1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [  0.000000] (0:maestro@) Path = 1;2;1;1;2;4;1;1;3;1
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2;1;1;2;4;1;1;3;1'
 > [  0.000000] (0:maestro@) DFS exploration ended. 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
\ No newline at end of file

diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
index 9badbef..e8b5ceb 100644 (file)
--- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
+++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
@@ -551,5 +551,5 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.
 > [  0.000000] (0:maestro@)   1: iRecv(mbox=0)
 > [  0.000000] (0:maestro@)   3: iSend(mbox=0)
 > [  0.000000] (0:maestro@)   1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [  0.000000] (0:maestro@) Path = 1;3;1;3;1;3;1
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;3;1;3;1'
 > [  0.000000] (0:maestro@) DFS exploration ended. 1006 unique states visited; 350 backtracks (5319 transition replays, 3963 states visited overall)

diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh
index 912b9a1..0cfec07 100644 (file)
--- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh
+++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh
@@ -15,6 +15,6 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none -- ${bin
 > [0.000000] [mc_ModelChecker/INFO]   1: iRecv(mbox=0)
 > [0.000000] [mc_ModelChecker/INFO]   2: iSend(mbox=0)
 > [0.000000] [mc_ModelChecker/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [0.000000] [mc_ModelChecker/INFO] Path = 1;3;1;1;2;1
+> [0.000000] [mc_ModelChecker/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 119 unique states visited; 36 backtracks (330 transition replays, 175 states visited overall)
 

diff --git a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh
index d49289d..fc687a9 100644 (file)
--- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh
+++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh
@@ -22,5 +22,5 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-assert ${plat
 > [  0.000000] (0:maestro@)   1: iRecv(mbox=0)
 > [  0.000000] (0:maestro@)   2: iSend(mbox=0)
 > [  0.000000] (0:maestro@)   1: WaitComm(from 2 to 1, mbox=0, no timeout)
-> [  0.000000] (0:maestro@) Path = 1;3;1;1;2;1
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;2;1'
 > [  0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 4 backtracks (36 transition replays, 14 states visited overall)

diff --git a/examples/smpi/mc/sendsend.tesh b/examples/smpi/mc/sendsend.tesh
index c1ca35f..26c90a3 100644 (file)
--- a/examples/smpi/mc/sendsend.tesh
+++ b/examples/smpi/mc/sendsend.tesh
@@ -22,6 +22,6 @@ $ ../../../smpi_script/bin/smpirun -quiet -wrapper "${bindir:=.}/../../../bin/si
 > [0.000000] [mc_global/INFO] Counter-example execution trace:
 > [0.000000] [mc_global/INFO]   1: iSend(mbox=2)
 > [0.000000] [mc_global/INFO]   2: iSend(mbox=0)
-> [0.000000] [mc_global/INFO] Path = 1;2
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;2'
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
 > Execution failed with code 3.

diff --git a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
index 63ff776..eba99b7 100644 (file)
--- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
+++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
@@ -22,5 +22,5 @@ $ ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir
 > [0.000000] [mc_global/INFO]   2: MUTEX_ASYNC_LOCK(mutex: 1, owner:3)
 > [0.000000] [mc_global/INFO]   3: MUTEX_WAIT(mutex: 1, owner:3)
 > [0.000000] [mc_global/INFO]   3: MUTEX_ASYNC_LOCK(mutex: 0, owner:2)
-> [0.000000] [mc_global/INFO] Path = 2;2;3;2;3;3
+> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3'
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 2 backtracks (22 transition replays, 2 states visited overall)

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 17e2bce..eac05cd 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -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);

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 27518c4..08e5c85 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -204,7 +204,9 @@ void RemoteApp::check_deadlock() const
     XBT_CINFO(mc_global, "Counter-example execution trace:");
     for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
       XBT_CINFO(mc_global, "  %s", frame.c_str());
-    XBT_CINFO(mc_global, "Path = %s", model_checker_->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'",
+             model_checker_->get_exploration()->get_record_trace().to_string().c_str());
     model_checker_->get_exploration()->log_state();
     throw DeadlockError();
   }

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index e0628c0..3af39bc 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -49,7 +49,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();

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 8f1ecb2..03ec2d0 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -275,7 +275,9 @@ void LivenessChecker::show_acceptance_cycle(std::size_t depth)
   XBT_INFO("Counter-example that violates formula:");
   for (auto const& s : this->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();
   XBT_INFO("Counter-example depth: %zu", depth);
 }

diff --git a/teshsuite/mc/random-bug/random-bug.tesh b/teshsuite/mc/random-bug/random-bug.tesh
index 3b6ffa2..952ba8e 100644 (file)
--- a/teshsuite/mc/random-bug/random-bug.tesh
+++ b/teshsuite/mc/random-bug/random-bug.tesh
@@ -9,7 +9,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir
 > [  0.000000] (0:maestro@) Counter-example execution trace:
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
-> [  0.000000] (0:maestro@) Path = 1/3;1/4
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
 
 ! expect return 6
@@ -24,7 +24,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}
 > [  0.000000] (0:maestro@) Counter-example execution trace:
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
-> [  0.000000] (0:maestro@) Path = 1/3;1/4
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
 
@@ -47,6 +47,6 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/
 > [  0.000000] (0:maestro@) Counter-example execution trace:
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
-> [  0.000000] (0:maestro@) Path = 1/3;1/4
+> [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc