From: Marion Guthmuller Date: Tue, 11 Dec 2012 17:01:54 +0000 (+0100) Subject: model-checker : update tesh bugged1_liveness X-Git-Tag: v3_9_rc1~86^2~123 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/8687b520f5bf89bedb3f7711d20ff70520221114?ds=sidebyside model-checker : update tesh bugged1_liveness --- diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index ac6e0b4709..97ff4e7c04 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -12,11 +12,11 @@ $ ${bindir:=.}/bugged1_liveness --cfg=model-check:1 --cfg=contexts/factory:ucont > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (3:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle -> [ 4.000000] (3:client@Boivin) Ask the request +> [ 0.000000] (3:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly -> [ 4.000000] (3:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (3:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle -> [ 8.000000] (3:client@Boivin) Ask the request +> [ 0.000000] (3:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (0:@) Next pair (depth = 33, 2 interleave) already reached ! > [ 0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*