From: Martin Quinson Date: Tue, 1 Nov 2022 21:16:35 +0000 (+0100) Subject: MC: tell the user about how to use the replay path in case of problem X-Git-Tag: v3.34~720 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/b2ec476dd5313063d2f6b15d7ef4a16077e46355 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 bd135cf7bf..97ec9d5b62 100644 --- 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 9badbef5d1..e8b5ceb102 100644 --- 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 912b9a158b..0cfec07f8a 100644 --- 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 d49289dafb..fc687a94cc 100644 --- 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 c1ca35ff21..26c90a3e1c 100644 --- 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 63ff7761ca..eba99b78b4 100644 --- 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 17e2bce738..eac05cd7d4 100644 --- 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 27518c41f8..08e5c851fc 100644 --- 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 e0628c0953..3af39bc674 100644 --- 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 8f1ecb22d9..03ec2d033d 100644 --- 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 3b6ffa213b..952ba8ebe3 100644 --- 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