From 123e2bc0a77b339a9ad80db0e07ab2e647677a40 Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 12 Oct 2009 16:09:34 +0000 Subject: [PATCH] firewire git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1530 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/firewire/abst/auto | 10 +++--- prism-examples/firewire/abst/deadline.nm | 38 +++++++++++----------- prism-examples/firewire/abst/deadline.pctl | 2 +- prism-examples/firewire/abst/expected.pctl | 2 +- 4 files changed, 26 insertions(+), 26 deletions(-) diff --git a/prism-examples/firewire/abst/auto b/prism-examples/firewire/abst/auto index 84f2ef0b..bcb1adfc 100755 --- a/prism-examples/firewire/abst/auto +++ b/prism-examples/firewire/abst/auto @@ -1,15 +1,15 @@ #!/bin/csh # liveness -prism firewire.nm liveness.pctl -const delay=36,fast=0.5 -m +prism firewire.nm liveness.pctl -const delay=36,fast=0.5 # maximum expected time -prism firewire.nm expected.pctl -const delay=3,fast=0.2:0.1:0.8 -m -prop 1 -prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 1 +prism firewire.nm expected.pctl -const delay=3,fast=0.2:0.1:0.8 -prop 1 +prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -prop 1 # maximum expected time -prism firewire.nm expected.pctl -const delay=3,fast=0.2:0.1:0.8 -m -prop 2 -prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 2 +prism firewire.nm expected.pctl -const delay=3,fast=0.2:0.1:0.8 -prop 2 +prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -prop 2 # deadline properties foreach deadline (200 300 400 500 600) # 800 1000) diff --git a/prism-examples/firewire/abst/deadline.nm b/prism-examples/firewire/abst/deadline.nm index cd217a1f..619053a0 100644 --- a/prism-examples/firewire/abst/deadline.nm +++ b/prism-examples/firewire/abst/deadline.nm @@ -25,7 +25,7 @@ module abstract_firewire x : [0..kx+1]; // local state - s : [0..10]; + s : [0..11]; // 0 -start_start // 1 -fast_start // 2 -start_fast @@ -35,45 +35,45 @@ module abstract_firewire // 6 -fast_slow // 7 -slow_fast // 8 -slow_slow - // 9 -done - // 10 - passed deadline + // 9 -seldone + // 10 -done_before + // 11 -done_after // initial state [] (s=0) & (x (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=0) & (y<=deadline) -> fast : (s'=1) + slow : (s'=4); - [] (s=0) & (y<=deadline) -> fast : (s'=2) + slow : (s'=3); + [] (s=0) -> fast : (s'=1) + slow : (s'=4); + [] (s=0) -> fast : (s'=2) + slow : (s'=3); // fast_start [] (s=1) & (x (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=1) & (y<=deadline) -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0); + [] (s=1) -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0); // start_fast [] (s=2) & (x (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=2) & (y<=deadline) -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0); + [] (s=2) -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0); // start_slow [] (s=3) & (x (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=3) & (y<=deadline) -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0); + [] (s=3) -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0); // slow_start [] (s=4) & (x (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=4) & (y<=deadline) -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0); + [] (s=4) -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0); // fast_fast [] (s=5) & (x<85) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=5) & (x>=76) & (y<=deadline) -> (s'=0) & (x'=0); - [] (s=5) & (x>=76-delay) & (y<=deadline) -> (s'=9) & (x'=0); + [] (s=5) & (x>=76) -> (s'=0) & (x'=0); + [] (s=5) & (x>=76-delay) -> (s'=9) & (x'=0); // fast_slow [] (s=6) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=6) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0); + [] (s=6) & (x>=159-delay) -> (s'=9) & (x'=0); // slow_fast [] (s=7) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=7) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0); + [] (s=7) & (x>=159-delay) -> (s'=9) & (x'=0); // slow_slow [] (s=8) & (x<167) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=8) & (x>=159) & (y<=deadline) -> (s'=0) & (x'=0); - [] (s=8) & (x>=159-delay) & (y<=deadline) -> (s'=9) & (x'=0); + [] (s=8) & (x>=159) -> (s'=0) & (x'=0); + [] (s=8) & (x>=159-delay) -> (s'=9) & (x'=0); // move to deadline exceeded when y>=deadline - [] (y>deadline) & (s<9) -> (s'=10) & (y'=0); + [] (y<=deadline) & (s=9) -> (s'=10) & (y'=0); + [] (y>deadline) & (s=9) -> (s'=11) & (y'=0); // done - [] (s=9) -> (s'=9); - // deadline exceeded - [] (s=10) -> (s'=10); + [] (s>=10) -> true; endmodule diff --git a/prism-examples/firewire/abst/deadline.pctl b/prism-examples/firewire/abst/deadline.pctl index 60e82520..c416e0c6 100644 --- a/prism-examples/firewire/abst/deadline.pctl +++ b/prism-examples/firewire/abst/deadline.pctl @@ -1,2 +1,2 @@ // deadline property -Pmin=?[ true U (s=9) ] +Pmin=?[ true U (s=10) ] diff --git a/prism-examples/firewire/abst/expected.pctl b/prism-examples/firewire/abst/expected.pctl index de3d9006..202d8d20 100644 --- a/prism-examples/firewire/abst/expected.pctl +++ b/prism-examples/firewire/abst/expected.pctl @@ -1,4 +1,4 @@ // maximum expected time -R{"time"}max=?[F (s=9) ] +R{"time"}min=?[F (s=9) ] // maximum expected rounds R{"rounds"}max=?[F (s=9) ]