Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Fix stat missorder at the end of DFSexplorer
[simgrid.git] / examples / cpp / mc-failing-assert / s4u-mc-failing-assert-nodpor.tesh
1 #!/usr/bin/env tesh
2
3 ! expect return 1
4 ! timeout 300
5 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
6 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
7 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none.
8 > [0.000000] [mc_explo/INFO] **************************
9 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
10 > [0.000000] [mc_explo/INFO] **************************
11 > [0.000000] [mc_explo/INFO] Counter-example execution trace:
12 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
13 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
14 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
15 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
16 > [0.000000] [mc_explo/INFO]   2: iSend(mbox=0)
17 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
18 > [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'
19 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 119 unique states visited; 36 backtracks (175 transition replays, 330 states visited overall)
20
21 ! expect return 1
22 ! timeout 300
23 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:max_match_comm -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
24 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
25 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'max_match_comm'
26 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none.
27 > [0.000000] [mc_explo/INFO] **************************
28 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
29 > [0.000000] [mc_explo/INFO] **************************
30 > [0.000000] [mc_explo/INFO] Counter-example execution trace:
31 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
32 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
33 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
34 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
35 > [0.000000] [mc_explo/INFO]   2: iSend(mbox=0)
36 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
37 > [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;1;1;1;2;1'
38 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 29 unique states visited; 5 backtracks (17 transition replays, 51 states visited overall)
39
40
41 ! expect return 1
42 ! timeout 300
43 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:min_match_comm -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
44 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
45 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'min_match_comm'
46 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none.
47 > [0.000000] [mc_explo/INFO] **************************
48 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
49 > [0.000000] [mc_explo/INFO] **************************
50 > [0.000000] [mc_explo/INFO] Counter-example execution trace:
51 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
52 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
53 > [0.000000] [mc_explo/INFO]   2: iSend(mbox=0)
54 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
55 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
56 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
57 > [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;1;1'
58 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 backtracks (1 transition replays, 15 states visited overall)
59
60 ! expect return 1
61 ! timeout 300
62 $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/reduction:none --cfg=model-check/strategy:uniform --cfg=model-check/rand-seed:42 -- ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml --log=root.thresh:critical
63 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
64 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'uniform'
65 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/rand-seed' to '42'
66 > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: none.
67 > [0.000000] [mc_explo/INFO] **************************
68 > [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
69 > [0.000000] [mc_explo/INFO] **************************
70 > [0.000000] [mc_explo/INFO] Counter-example execution trace:
71 > [0.000000] [mc_explo/INFO]   3: iSend(mbox=0)
72 > [0.000000] [mc_explo/INFO]   2: iSend(mbox=0)
73 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
74 > [0.000000] [mc_explo/INFO]   3: WaitComm(from 3 to 1, mbox=0, no timeout)
75 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 3 to 1, mbox=0, no timeout)
76 > [0.000000] [mc_explo/INFO]   1: iRecv(mbox=0)
77 > [0.000000] [mc_explo/INFO]   1: WaitComm(from 2 to 1, mbox=0, no timeout)
78 > [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;3;1;1;1'
79 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 44 unique states visited; 7 backtracks (19 transition replays, 70 states visited overall)