From 2b329118ba075ec2aedefb3062236e138a5ba574 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 12 Mar 2023 23:59:42 +0100 Subject: [PATCH] Move another function out of ModelChecker --- examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh | 24 +++++++++---------- .../s4u-mc-failing-assert-nodpor.tesh | 22 ++++++++--------- src/mc/ModelChecker.cpp | 13 ++-------- src/mc/explo/Exploration.cpp | 14 +++++++++++ src/mc/explo/Exploration.hpp | 2 ++ 5 files changed, 41 insertions(+), 34 deletions(-) diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh index d64aed948f..a104fb8463 100644 --- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh +++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh @@ -4,16 +4,16 @@ ! timeout 20 $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml --log=root.thresh:critical --log=mc.thresh:info > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor. -> [0.000000] [mc_ModelChecker/INFO] ************************** -> [0.000000] [mc_ModelChecker/INFO] *** PROPERTY NOT VALID *** -> [0.000000] [mc_ModelChecker/INFO] ************************** -> [0.000000] [mc_ModelChecker/INFO] Counter-example execution trace: -> [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) -> [0.000000] [mc_ModelChecker/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [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;3;3;1' +> [0.000000] [mc_explo/INFO] ************************** +> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** +> [0.000000] [mc_explo/INFO] ************************** +> [0.000000] [mc_explo/INFO] Counter-example execution trace: +> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/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;3;3;1' > [0.000000] [mc_dfs/INFO] DFS exploration ended. 2091 unique states visited; 529 backtracks (8359 transition replays, 5739 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 0cfec07f8a..c0d8fc031e 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 @@ -5,16 +5,16 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none' > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none. -> [0.000000] [mc_ModelChecker/INFO] ************************** -> [0.000000] [mc_ModelChecker/INFO] *** PROPERTY NOT VALID *** -> [0.000000] [mc_ModelChecker/INFO] ************************** -> [0.000000] [mc_ModelChecker/INFO] Counter-example execution trace: -> [0.000000] [mc_ModelChecker/INFO] 1: iRecv(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 3: iSend(mbox=0) -> [0.000000] [mc_ModelChecker/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) -> [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] 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_explo/INFO] ************************** +> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID *** +> [0.000000] [mc_explo/INFO] ************************** +> [0.000000] [mc_explo/INFO] Counter-example execution trace: +> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0) +> [0.000000] [mc_explo/INFO] 2: iSend(mbox=0) +> [0.000000] [mc_explo/INFO] 1: WaitComm(from 2 to 1, mbox=0, no timeout) +> [0.000000] [mc_explo/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/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 3f8db6157e..a59b3aa892 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -174,17 +174,8 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) return false; case MessageType::ASSERTION_FAILED: - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : get_exploration()->get_textual_trace()) - XBT_INFO(" %s", s.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(); - exploration_->system_exit(SIMGRID_MC_EXIT_SAFETY); + exploration_->report_assertion_failure(); + break; default: xbt_die("Unexpected message from model-checked application"); diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 3fc6127081..0e44b047a9 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -90,6 +90,20 @@ void Exploration::report_crash(int status) get_remote_app().get_remote_process_memory().terminate(); system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } +void Exploration::report_assertion_failure() +{ + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + for (auto const& s : get_textual_trace()) + XBT_INFO(" %s", s.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(); + system_exit(SIMGRID_MC_EXIT_SAFETY); +} void Exploration::system_exit(int status) { diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index 045c7c5ea2..ee3c452f1c 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -45,6 +45,8 @@ public: /** Produce an error message indicating that the application crashed (status was produced by waitpid) */ void report_crash(int status); + /** Produce an error message indicating that a property was violated */ + void report_assertion_failure(); /** Kill the application and the model-checker (which exits with `status`)*/ XBT_ATTRIB_NORETURN void system_exit(int status); -- 2.20.1