From 8687b520f5bf89bedb3f7711d20ff70520221114 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 11 Dec 2012 18:01:54 +0100 Subject: [PATCH] model-checker : update tesh bugged1_liveness --- examples/msg/mc/bugged1_liveness.tesh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-* -- 2.20.1