From 3eef1967487d565c4baae4d356599f833601c157 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Sun, 6 Oct 2013 23:29:54 +0200 Subject: [PATCH] model-checker : update tesh file --- examples/msg/mc/bugged1_liveness_visited.tesh | 52 ++++++++++++++++++- 1 file changed, 50 insertions(+), 2 deletions(-) diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh index 49d40fc57b..3341b5a9f4 100644 --- a/examples/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/msg/mc/bugged1_liveness_visited.tesh @@ -20,11 +20,57 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request. +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1) +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request. +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1) +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (1:coordinator@Tremblay) CS already used. Queue the request. +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1) +> [ 0.000000] (2:client@Boivin) Ask the request +> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle @@ -35,6 +81,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de > [ 0.000000] (1:coordinator@Tremblay) CS release. Grant to queued requests (queue size: 1) > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly +> [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle @@ -57,6 +104,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de > [ 0.000000] (2:client@Boivin) Ask the request > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it +> [ 0.000000] (3:client@Fafard) Propositions changed : r=1, cs=0 > [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly > [ 0.000000] (2:client@Boivin) 2 got the answer. Sleep a bit and release it > [ 0.000000] (1:coordinator@Tremblay) CS release. resource now idle @@ -129,5 +177,5 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de > [ 0.000000] (0:@) [(2)Boivin (client)] Wait(comm=(verbose only) [(1)Tremblay (coordinator)-> (2)Boivin (client)]) (62) > [ 0.000000] (0:@) [(2)Boivin (client)] iSend(src=(2)Boivin (client), buff=(verbose only), size=(verbose only)) (54) > [ 0.000000] (0:@) Expanded pairs = 57 -> [ 0.000000] (0:@) Visited pairs = 208 -> [ 0.000000] (0:@) Executed transitions = 207 \ No newline at end of file +> [ 0.000000] (0:@) Visited pairs = 365 +> [ 0.000000] (0:@) Executed transitions = 364 -- 2.20.1