]> AND Public Git Repository - simgrid.git/blobdiff - examples/cpp/mc-electric-fence/s4u-mc-electric-fence.tesh
Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Move an example to the right section, and document it
[simgrid.git] / examples / cpp / mc-electric-fence / s4u-mc-electric-fence.tesh
index 011b0c1912a8c8fcacb7a9ef79b7f6659483a7c6..e9742656886da9d65df174e40794ee34b99a29c7 100644 (file)
@@ -1,7 +1,7 @@
 #!/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!
@@ -9,7 +9,4 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${plat
 > [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!
-> [0.000000] [mc_safety/INFO] No property violation found.
-> [0.000000] [mc_safety/INFO] Expanded states = 15
-> [0.000000] [mc_safety/INFO] Visited states = 32
-> [0.000000] [mc_safety/INFO] Executed transitions = 14
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)