model-check/sleep-set is now true by default

diff --git a/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh b/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh
index 8f2d6cf..e956f9c 100644 (file)
--- a/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh
+++ b/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh
@@ -3,7 +3,7 @@
 ! expect return 2
 ! timeout 30
 ! output display
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 1 --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256  --cfg=model-check/property:promela_bugged1_liveness
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 1 --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request

diff --git a/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh b/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh
index 58d6358..5f0999c 100644 (file)
--- a/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh
+++ b/examples/cpp/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh
@@ -3,7 +3,7 @@
 ! expect return 2
 ! timeout 20
 ! output display
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 0 --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 0 --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request

diff --git a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
index a6593db..424e312 100644 (file)
--- a/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
+++ b/examples/cpp/mc-bugged1/s4u-mc-bugged1.tesh
@@ -9,13 +9,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/
 > [  0.000000] (1:server@HostA) OK
 > [  0.000000] (4:client@HostD) Sent!
 > [  0.000000] (2:client@HostB) Sent!
-> [  0.000000] (1:server@HostA) OK
-> [  0.000000] (3:client@HostC) Sent!
-> [  0.000000] (4:client@HostD) Sent!
-> [  0.000000] (2:client@HostB) Sent!
 > [  0.000000] (3:client@HostC) Sent!
-> [  0.000000] (1:server@HostA) OK
-> [  0.000000] (4:client@HostD) Sent!
 > [  0.000000] (2:client@HostB) Sent!
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
@@ -32,4 +26,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/
 > [  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@) 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. 26 unique states visited; 3 backtracks (20 transition replays, 49 states visited overall)
+> [  0.000000] (0:maestro@) DFS exploration ended. 19 unique states visited; 2 backtracks (12 transition replays, 33 states visited overall)

diff --git a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
index e1087e9..10cc2f3 100644 (file)
--- a/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
+++ b/examples/cpp/mc-bugged2/s4u-mc-bugged2.tesh
@@ -2,7 +2,7 @@
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${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
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${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_explo/INFO] **************************
 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
@@ -20,7 +20,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml  --log=root.thresh:critical --log=mc.thresh:info
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/strategy:min_match_comm ${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_explo/INFO] **************************
 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
@@ -39,7 +39,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml  --log=root.thresh:critical --log=mc.thresh:info
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/strategy:max_match_comm ${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_explo/INFO] **************************
 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***

diff --git a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
index bb5e3e1..8516a98 100644 (file)
--- a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
+++ b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
@@ -9,60 +9,6 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/
 > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
 > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
 > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
 > [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
 > [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
-> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 125 unique states visited; 20 backtracks (44 transition replays, 189 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 26 unique states visited; 6 backtracks (8 transition replays, 40 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 7c418cf..3b77074 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
@@ -16,7 +16,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 > [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 (175 transition replays, 330 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 24 unique states visited; 8 backtracks (26 transition replays, 58 states visited overall)
 
 ! expect return 1
 ! timeout 300
@@ -49,12 +49,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 > [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]   2: iSend(mbox=0)
-> [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
 > [0.000000] [mc_explo/INFO]   3: WaitComm(from 3 to 1, mbox=0, no timeout)
 > [0.000000] [mc_explo/INFO]   1: iRecv(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:'3;2;1;1;3;1;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (0 transition replays, 25 states visited overall)
\ No newline at end of file
+> [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;2;1;3;1;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 10 backtracks (26 transition replays, 65 states visited overall)
\ No newline at end of file

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 78bed01..fe7f6c9 100644 (file)
--- a/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh
+++ b/examples/cpp/mc-failing-assert/s4u-mc-failing-assert.tesh
@@ -2,7 +2,7 @@
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (2:client1@Bourassa) Sent!
 > [  0.000000] (1:server@Boivin) OK
@@ -23,7 +23,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/strategy:min_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (2:client1@Bourassa) Sent!
 > [  0.000000] (1:server@Boivin) OK
@@ -45,7 +45,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-c
 
 ! expect return 1
 ! timeout 20
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/strategy:max_match_comm ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (2:client1@Bourassa) Sent!
 > [  0.000000] (1:server@Boivin) OK

diff --git a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
index 6e8010b..b17f900 100644 (file)
--- a/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
+++ b/examples/cpp/synchro-barrier/s4u-mc-synchro-barrier.tesh
@@ -2,7 +2,9 @@
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
 > [Checker] Start a DFS exploration. Reduction is: dpor.
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 4).
 > [Checker] Execution came to an end at 1;1 (state: 3, depth: 3)
@@ -11,15 +13,19 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
 > [Checker] Start a DFS exploration. Reduction is: dpor.
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
 > [Checker] Dependent Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=3)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=3)
@@ -30,34 +36,23 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
 > [Checker] Execution came to an end at 1;2;1;2 (state: 5, depth: 5)
 > [Checker] Backtracking from 1;2;1;2
+> [Checker] Sleep set actually containing:
+> [Checker]   <1,BARRIER_ASYNC_LOCK(barrier: 0)>
 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
-> [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 6, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 3, state: 7, 0 interleaves)
-> [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=7)
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=7)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=8)
-> [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=6)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=8)
-> [Checker] 0 actors remain, but none of them need to be interleaved (depth 6).
-> [Checker] Execution came to an end at 2;1;1;2 (state: 9, depth: 5)
-> [Checker] Backtracking from 2;1;1;2
-> [Checker] DFS exploration ended. 9 unique states visited; 1 backtracks (0 transition replays, 10 states visited overall)
+> [Checker] 2 actors remain, but none of them need to be interleaved (depth 3).
+> [Checker] Backtracking from 2
+> [Checker] DFS exploration ended. 6 unique states visited; 1 backtracks (0 transition replays, 7 states visited overall)
 
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
 > [Checker] Start a DFS exploration. Reduction is: dpor.
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 3, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
@@ -65,10 +60,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] Dependent Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 5, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=4)
@@ -76,6 +73,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Dependent Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=3)
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=5)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 6, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_WAIT(barrier: 0) (state=5)
@@ -89,39 +87,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
 > [Checker] Execution came to an end at 1;2;3;1;2;3 (state: 7, depth: 7)
 > [Checker] Backtracking from 1;2;3;1;2;3
+> [Checker] Sleep set actually containing:
+> [Checker]   <2,BARRIER_ASYNC_LOCK(barrier: 0)>
 > [Checker] Execute 3: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
 > [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker] Execute 2: BARRIER_ASYNC_LOCK(barrier: 0) (stack depth: 3, state: 8, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=1)
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 4, state: 9, 0 interleaves)
-> [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=9)
-> [Checker] Execute 2: BARRIER_WAIT(barrier: 0) (stack depth: 5, state: 10, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=9)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=2)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker] Execute 3: BARRIER_WAIT(barrier: 0) (stack depth: 6, state: 11, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=10)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=11)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=9)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=11)
-> [Checker] Dependent Transitions:
-> [Checker]   BARRIER_ASYNC_LOCK(barrier: 0) (state=8)
-> [Checker]   BARRIER_WAIT(barrier: 0) (state=11)
-> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;3;2;1;2;3 (state: 12, depth: 7)
-> [Checker] Backtracking from 1;3;2;1;2;3
-> [Checker] DFS exploration ended. 12 unique states visited; 1 backtracks (1 transition replays, 14 states visited overall)
\ No newline at end of file
+> [Checker] 3 actors remain, but none of them need to be interleaved (depth 4).
+> [Checker] Backtracking from 1;3
+> [Checker] DFS exploration ended. 8 unique states visited; 1 backtracks (1 transition replays, 10 states visited overall)
\ No newline at end of file

diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh
index c67f1dc..d2a7187 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh
+++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex-stateful.tesh
@@ -2,9 +2,8 @@
 
 p This file tests the cfg=model-check/checkpoint option for DFS explorer
 
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/checkpoint:5 --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/checkpoint:5 -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/checkpoint' to '5'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (22 transition replays, 99 states visited overall)

diff --git a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
index dd4f3c1..f7f1a55 100644 (file)
--- a/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
+++ b/examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
@@ -5,9 +5,13 @@ p This file tests the dependencies between MUTEX transitions
 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
 > [App    ] Configuration change: Set 'actors' to '1'
 > [Checker] Start a DFS exploration. Reduction is: dpor.
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 1, state: 1, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 2, state: 2, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 3, state: 3, 0 interleaves)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 4, state: 4, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
@@ -18,10 +22,12 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
 > [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=4)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 5, 0 interleaves)
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
 > [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=5)
+> [Checker] Sleep set actually containing:
 > [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 6, 0 interleaves)
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=3)
@@ -29,6 +35,8 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
 > [Checker] Execution came to an end at 1;1;1;2;2;2 (state: 7, depth: 7)
 > [Checker] Backtracking from 1;1;1;2;2;2
+> [Checker] Sleep set actually containing:
+> [Checker]   <1,MUTEX_UNLOCK(mutex: 0, owner: -1)>
 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (stack depth: 3, state: 3, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
 > [Checker]   MUTEX_WAIT(mutex: 0, owner: 1) (state=2)
@@ -36,49 +44,42 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=1)
 > [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: 2) (stack depth: 4, state: 8, 0 interleaves)
-> [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 1) (state=3)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 5, state: 9, 0 interleaves)
-> [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=9)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 10, 0 interleaves)
-> [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 2) (state=8)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=10)
-> [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 1;1;2;1;2;2 (state: 11, depth: 7)
-> [Checker] Backtracking from 1;1;2;1;2;2
+> [Checker] 2 actors remain, but none of them need to be interleaved (depth 5).
+> [Checker] Backtracking from 1;1;2
+> [Checker] Sleep set actually containing:
+> [Checker]   <1,MUTEX_ASYNC_LOCK(mutex: 0, owner: 1)>
 > [Checker] Execute 2: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 1, state: 1, 0 interleaves)
-> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 12, 0 interleaves)
+> [Checker] Sleep set actually containing:
+> [Checker] Execute 1: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (stack depth: 2, state: 9, 0 interleaves)
 > [Checker] Dependent Transitions:
 > [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=1)
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 13, 0 interleaves)
+> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker] Sleep set actually containing:
+> [Checker] Execute 2: MUTEX_WAIT(mutex: 0, owner: 2) (stack depth: 3, state: 10, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=13)
-> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 14, 0 interleaves)
+> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner: 2) (state=10)
+> [Checker] Sleep set actually containing:
+> [Checker] Execute 2: MUTEX_UNLOCK(mutex: 0, owner: 1) (stack depth: 4, state: 11, 0 interleaves)
 > [Checker] INDEPENDENT Transitions:
-> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=12)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 15, 0 interleaves)
+> [Checker]   MUTEX_ASYNC_LOCK(mutex: 0, owner: 2) (state=9)
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker] Sleep set actually containing:
+> [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner: 1) (stack depth: 5, state: 12, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker]   MUTEX_WAIT(mutex: 0, owner: 1) (state=15)
-> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 16, 0 interleaves)
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker]   MUTEX_WAIT(mutex: 0, owner: 1) (state=12)
+> [Checker] Sleep set actually containing:
+> [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner: -1) (stack depth: 6, state: 13, 0 interleaves)
 > [Checker] Dependent Transitions:
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=14)
-> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=16)
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: 1) (state=11)
+> [Checker]   MUTEX_UNLOCK(mutex: 0, owner: -1) (state=13)
 > [Checker] 0 actors remain, but none of them need to be interleaved (depth 8).
-> [Checker] Execution came to an end at 2;1;2;2;1;1 (state: 17, depth: 7)
+> [Checker] Execution came to an end at 2;1;2;2;1;1 (state: 14, depth: 7)
 > [Checker] Backtracking from 2;1;2;2;1;1
-> [Checker] DFS exploration ended. 17 unique states visited; 2 backtracks (2 transition replays, 21 states visited overall)
+> [Checker] DFS exploration ended. 14 unique states visited; 2 backtracks (2 transition replays, 18 states visited overall)
 
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (49 transition replays, 126 states visited overall)

diff --git a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
index 3a82897..65836b1 100644 (file)
--- a/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
+++ b/examples/cpp/synchro-semaphore/s4u-mc-synchro-semaphore.tesh
@@ -1,6 +1,5 @@
 #!/usr/bin/env tesh
 
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --log=mc_dfs.thres:info --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
-> [Checker] Configuration change: Set 'model-check/sleep-set' to 'true'
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:info --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
 > [Checker] Start a DFS exploration. Reduction is: dpor.
 > [Checker] DFS exploration ended. 33 unique states visited; 8 backtracks (84 transition replays, 125 states visited overall)

diff --git a/examples/sthread/pthread-mc-mutex-simple.tesh b/examples/sthread/pthread-mc-mutex-simple.tesh
index 6e5bc5f..55ecc95 100644 (file)
--- a/examples/sthread/pthread-mc-mutex-simple.tesh
+++ b/examples/sthread/pthread-mc-mutex-simple.tesh
@@ -9,10 +9,7 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > The thread 0 is terminating.
 > The thread 1 is terminating.
 > User's main is terminating.
-> The thread 0 is terminating.
-> The thread 1 is terminating.
-> User's main is terminating.
 > The thread 1 is terminating.
 > The thread 0 is terminating.
 > User's main is terminating.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (2 transition replays, 27 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 18 unique states visited; 2 backtracks (2 transition replays, 22 states visited overall)
\ No newline at end of file

diff --git a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
index 5e6cac0..e95629c 100644 (file)
--- a/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
+++ b/examples/sthread/pthread-mc-mutex-simpledeadlock.tesh
@@ -12,12 +12,6 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > The thread 0 is terminating.
 > The thread 1 is terminating.
 > User's main is terminating.
-> The thread 0 is terminating.
-> The thread 1 is terminating.
-> User's main is terminating.
-> The thread 0 is terminating.
-> The thread 1 is terminating.
-> User's main is terminating.
 > [0.000000] [mc_global/INFO] **************************
 > [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
 > [0.000000] [mc_global/INFO] **************************
@@ -34,4 +28,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec
 > [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_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. 38 unique states visited; 3 backtracks (11 transition replays, 52 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 21 unique states visited; 3 backtracks (11 transition replays, 35 states visited overall)
\ No newline at end of file

diff --git a/examples/sthread/stdobject/stdobject.tesh b/examples/sthread/stdobject/stdobject.tesh
index da50b77..fefbd72 100644 (file)
--- a/examples/sthread/stdobject/stdobject.tesh
+++ b/examples/sthread/stdobject/stdobject.tesh
@@ -4,8 +4,7 @@
 # We ignore the LD_PRELOAD lines from the expected output because they contain the build path
 ! ignore .*LD_PRELOAD.*
 
-$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/stdobject "--log=root.fmt:[%11.6r]%e(%a@%h)%e%m%n" --log=no_loc
-> [   0.000000] (maestro@) Configuration change: Set 'model-check/sleep-set' to 'true'
+$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/stdobject "--log=root.fmt:[%11.6r]%e(%a@%h)%e%m%n" --log=no_loc
 > [   0.000000] (maestro@) Starting the simulation.
 > starting two helpers...
 > waiting for helpers to finish...

diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp
index 571ec6e..cdba765 100644 (file)
--- a/src/mc/mc_config.cpp
+++ b/src/mc/mc_config.cpp
@@ -57,13 +57,13 @@ int _sg_mc_max_visited_states = 0;
 static simgrid::config::Flag<std::string> cfg_mc_reduction{
     "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
     [](std::string_view value) {
-      if (value != "none" && value != "dpor" && value != "sdpor" && value != "odpor")
+      if (value != "none" && value != "dpor" && value != "sdpor" && value != "odpor" && value != "udpor")
         xbt_die("configuration option 'model-check/reduction' must be one of the following: "
-                " 'none', 'dpor', 'sdpor', or 'odpor'");
+                " 'none', 'dpor', 'sdpor', 'odpor', or 'udpor'");
     }};
 
 simgrid::config::Flag<bool> _sg_mc_sleep_set{
-    "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", false,
+    "model-check/sleep-set", "Whether to enable the use of sleep-set in the reduction algorithm", true,
     [](bool) { _mc_cfg_cb_check("value to enable/disable the use of sleep-set in the reduction algorithm"); }};
 
 simgrid::config::Flag<std::string> _sg_mc_strategy{

diff --git a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
index 740b47a..ecdacc4 100644 (file)
--- a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
+++ b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
@@ -1,7 +1,7 @@
 # Smpi Allreduce collectives tests
 
 p Test allreduce
-$ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -map -hostfile ../hostfile_coll -platform  ${platfdir:=.}/small_platform.xml --cfg=model-check/sleep-set:true -np 4 --log=xbt_cfg.thres:critical ${bindir:=.}/coll-allreduce-with-leaks --log=smpi_config.thres:warning --cfg=smpi/display-allocs:yes --cfg=smpi/simulate-computation:no --log=smpi_coll.thres:error --log=smpi_mpi.thres:error --cfg=smpi/list-leaks:10 --log=no_loc
+$ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -map -hostfile ../hostfile_coll -platform  ${platfdir:=.}/small_platform.xml -np 4 --log=xbt_cfg.thres:critical ${bindir:=.}/coll-allreduce-with-leaks --log=smpi_config.thres:warning --cfg=smpi/display-allocs:yes --cfg=smpi/simulate-computation:no --log=smpi_coll.thres:error --log=smpi_mpi.thres:error --cfg=smpi/list-leaks:10 --log=no_loc
 > [0.000000] [smpi/INFO] [rank 0] -> Tremblay
 > [0.000000] [smpi/INFO] [rank 1] -> Tremblay
 > [0.000000] [smpi/INFO] [rank 2] -> Tremblay