From 713ee3aaf79f61905c8b0df05e5e787a525ebef2 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Mon, 8 Aug 2022 01:39:35 +0200 Subject: [PATCH] Add tests of state equality reduction and nodpor for DFS explo --- MANIFEST.in | 7 ++----- examples/cpp/CMakeLists.txt | 21 +++++++++++++++++++ .../s4u-mc-failing-assert-nodpor.tesh | 20 ++++++++++++++++++ .../s4u-mc-failing-assert-statequality.tesh | 19 +++++++++++++++++ 4 files changed, 62 insertions(+), 5 deletions(-) create mode 100644 examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh create mode 100644 examples/cpp/mc-failing-assert/s4u-mc-failing-assert-statequality.tesh diff --git a/MANIFEST.in b/MANIFEST.in index 60fb437409..7a3784fcef 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -316,6 +316,8 @@ include examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.cpp include examples/cpp/mc-centralized-mutex/s4u-mc-centralized-mutex.tesh include examples/cpp/mc-electric-fence/s4u-mc-electric-fence.cpp include examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh +include examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh +include examples/cpp/mc-failing-assert/s4u-mc-failing-assert-statequality.tesh include examples/cpp/mc-failing-assert/s4u-mc-failing-assert.cpp include examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh include examples/cpp/network-factors/s4u-network-factors.cpp @@ -2280,8 +2282,6 @@ include src/mc/ModelChecker.cpp include src/mc/ModelChecker.hpp include src/mc/VisitedState.cpp include src/mc/VisitedState.hpp -include src/mc/api.cpp -include src/mc/api.hpp include src/mc/api/ActorState.hpp include src/mc/api/RemoteApp.cpp include src/mc/api/RemoteApp.hpp @@ -2324,14 +2324,11 @@ include src/mc/mc_config.hpp include src/mc/mc_exit.hpp include src/mc/mc_forward.hpp include src/mc/mc_global.cpp -include src/mc/mc_hash.cpp -include src/mc/mc_hash.hpp include src/mc/mc_mmu.hpp include src/mc/mc_private.hpp include src/mc/mc_record.cpp include src/mc/mc_record.hpp include src/mc/mc_replay.hpp -include src/mc/mc_safety.hpp include src/mc/remote/AppSide.cpp include src/mc/remote/AppSide.hpp include src/mc/remote/Channel.cpp diff --git a/examples/cpp/CMakeLists.txt b/examples/cpp/CMakeLists.txt index bc8952b46a..1d4bb98e01 100644 --- a/examples/cpp/CMakeLists.txt +++ b/examples/cpp/CMakeLists.txt @@ -213,6 +213,27 @@ foreach(example app-bittorrent app-masterworkers ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}.tesh) endforeach() +# Test non-DPOR reductions on a given MC test +if(SIMGRID_HAVE_MC) + foreach(example mc-failing-assert) + ADD_TESH(s4u-${example}-statequality --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} + --setenv libdir=${CMAKE_BINARY_DIR}/lib + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh) + set(tesh_files ${tesh_files} ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-statequality.tesh) + + ADD_TESH(s4u-${example}-nodpor --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example} + --setenv libdir=${CMAKE_BINARY_DIR}/lib + --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms + --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}/${example} + --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example} + ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh) + set(tesh_files ${tesh_files} ${CMAKE_HOME_DIRECTORY}/examples/cpp/${example}/s4u-${example}-nodpor.tesh) + endforeach() +endif() + # Examples not accepting factories ################################## 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 new file mode 100644 index 0000000000..912b9a158b --- /dev/null +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-nodpor.tesh @@ -0,0 +1,20 @@ +#!/usr/bin/env tesh + +! expect return 1 +! timeout 300 +$ ${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] Path = 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-statequality.tesh b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-statequality.tesh new file mode 100644 index 0000000000..5489a1e182 --- /dev/null +++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert-statequality.tesh @@ -0,0 +1,19 @@ +#!/usr/bin/env tesh + +! expect return 1 +! timeout 300 +$ ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/visited:20 -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical +> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/visited' to '20' +> [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] 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_dfs/INFO] DFS exploration ended. 18 unique states visited; 4 backtracks (22 transition replays, 0 states visited overall) -- 2.20.1