From badfaf9202e51461e7a685e17ce982ea34ad219a Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 24 Oct 2013 15:43:18 +0200 Subject: [PATCH] model-checker : update tesh files --- examples/msg/mc/bugged1_liveness.tesh | 2 +- examples/msg/mc/bugged1_liveness_visited.tesh | 53 ++----------------- 2 files changed, 4 insertions(+), 51 deletions(-) diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index 3413fbb5bb..63bee18665 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -43,7 +43,7 @@ $ ${bindir:=.}/bugged1_liveness ${bindir:=.}/../msg_platform.xml ${bindir:=.}/de > [ 0.000000] (0:@) Expanded pairs = 21 > [ 0.000000] (0:@) Visited pairs = 21 > [ 0.000000] (0:@) Executed transitions = 20 - +> [ 0.000000] (0:@) Counter-example depth : 20 diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh index 3341b5a9f4..25377200eb 100644 --- a/examples/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/msg/mc/bugged1_liveness_visited.tesh @@ -20,57 +20,11 @@ $ ${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 @@ -81,7 +35,6 @@ $ ${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 @@ -104,7 +57,6 @@ $ ${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 @@ -177,5 +129,6 @@ $ ${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 = 365 -> [ 0.000000] (0:@) Executed transitions = 364 +> [ 0.000000] (0:@) Visited pairs = 208 +> [ 0.000000] (0:@) Executed transitions = 207 +> [ 0.000000] (0:@) Counter-example depth : 50 -- 2.20.1