X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/eb6d2036ae2c22f06f32bf4aba3e165a0d110fbe..b519c710a179e22b19c6d21721c6c0dfd13e65ce:/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh

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 d402818267..7c759478b0 100644
--- a/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
+++ b/examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
@@ -1,13 +1,92 @@
 #!/usr/bin/env tesh
 
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${platfdir}/model_checker_platform.xml
-> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [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!
+> [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!
+> [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!
+> [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!
+> [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!
+> [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!
+> [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!
+> [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!
+> [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!
+> [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!
-> [0.000000] [mc_safety/INFO] No property violation found.
-> [0.000000] [mc_safety/INFO] 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 169 unique states visited; 28 backtracks (261 transition replays, 64 states visited overall)
\ No newline at end of file