Add tests of state equality reduction and nodpor for DFS explo

diff --git a/MANIFEST.in b/MANIFEST.in
index 60fb437..7a3784f 100644 (file)
--- 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 bc8952b..1d4bb98 100644 (file)
--- 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 (file)
index 0000000..912b9a1
--- /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 (file)
index 0000000..5489a1e
--- /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)