From 7b195d996d99b7aebde14673742f45d7cfb3e13f Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Fri, 5 Dec 2008 11:58:20 +0000 Subject: [PATCH] expected properties added to firewire abstion version git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@846 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/firewire/abst/auto | 10 +- prism-examples/firewire/abst/deadline.nm | 143 ++++++++++++----------- prism-examples/firewire/abst/firewire.nm | 121 ++++++++++--------- 3 files changed, 151 insertions(+), 123 deletions(-) diff --git a/prism-examples/firewire/abst/auto b/prism-examples/firewire/abst/auto index 86de3804..422b42c6 100755 --- a/prism-examples/firewire/abst/auto +++ b/prism-examples/firewire/abst/auto @@ -1,9 +1,15 @@ #!/bin/csh # liveness -prism firewire.nm liveness.pctl -m +prism firewire.nm liveness.pctl -const delay=36,fast=0.5 -m + +# maximum expected time +prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 1 + +# maximum expected time +prism firewire.nm expected.pctl -const delay=36,fast=0.2:0.1:0.8 -m -prop 1 # deadline properties foreach deadline (200 300 400 500 600) # 800 1000) - prism deadline.nm deadline.pctl -const deadline=$deadline -m + prism deadline.nm deadline.pctl -const deadline=$deadline,delay=36,fast=0.5 -m end diff --git a/prism-examples/firewire/abst/deadline.nm b/prism-examples/firewire/abst/deadline.nm index 7ebe3e84..cd217a1f 100644 --- a/prism-examples/firewire/abst/deadline.nm +++ b/prism-examples/firewire/abst/deadline.nm @@ -1,74 +1,79 @@ -// integer semantics version of abstract firewire protocol +// integer semantics version of abstract firewire protocol +// with clock for deadline properties // gxn 23/05/2001 mdp -//deadline -const int deadline; - -// largest constant the deadline clock is compared to -const int ky = deadline; - -// largest constant the clock of the system is compared to -const int kx = 167; - -module abstract_firewire - - // deadline clock - y : [0..ky+1]; - - // clock of the system - x : [0..kx+1]; - - // local state - s : [0..10]; - // 0 - start_start - // 1 - fast_start - // 2 - start_fast - // 3 - start_slow - // 4 - slow_start - // 5 - fast_fast - // 6 - fast_slow - // 7 - slow_fast - // 8 - slow_slow - // 9 - done - // 10 - deadline exceeded - - // initial state - [] (s=0) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=0) & (y<=deadline) -> 0.5 : (s'=1) + 0.5 : (s'=4); - [] (s=0) & (y<=deadline) -> 0.5 : (s'=2) + 0.5 : (s'=3); - // fast_start - [] (s=1) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=1) & (y<=deadline) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=6) & (x'=0); - // start_fast - [] (s=2) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=2) & (y<=deadline) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=7) & (x'=0); - // start_slow - [] (s=3) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=3) & (y<=deadline) -> 0.5 : (s'=6) & (x'=0) + 0.5 : (s'=8) & (x'=0); - // slow_start - [] (s=4) & (x<36) -> (x'=min(x+1,kx+1)) & (y'=min(y+1,ky+1)); - [] (s=4) & (y<=deadline) -> 0.5 : (s'=7) & (x'=0) + 0.5 : (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>=40) & (y<=deadline) -> (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>=123) & (y<=deadline) -> (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>=123) & (y<=deadline) -> (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>=123) & (y<=deadline) -> (s'=9) & (x'=0); - // move to deadline exceeded when y>=deadline - [] (y>=deadline) -> (s'=10); - // done - [] (s=9) -> (s'=9); - // deadline exceeded - [] (s=10) -> (s'=10); - +// deadline +const int deadline; +const int ky = deadline; +// wire delay (based on max length of wire) +const int delay; +// probability of choosing fast +const double fast; +const double slow = 1-fast; + +// maximal constant +const int kx = 167; + +module abstract_firewire + + // deadline clock + y : [0..ky+1]; + + // model clock + x : [0..kx+1]; + + // local state + s : [0..10]; + // 0 -start_start + // 1 -fast_start + // 2 -start_fast + // 3 -start_slow + // 4 -slow_start + // 5 -fast_fast + // 6 -fast_slow + // 7 -slow_fast + // 8 -slow_slow + // 9 -done + // 10 - passed deadline + + // 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); + // 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); + // 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); + // 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); + // 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); + // 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); + // 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); + // 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); + // 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); + + // move to deadline exceeded when y>=deadline + [] (y>deadline) & (s<9) -> (s'=10) & (y'=0); + // done + [] (s=9) -> (s'=9); + // deadline exceeded + [] (s=10) -> (s'=10); + endmodule diff --git a/prism-examples/firewire/abst/firewire.nm b/prism-examples/firewire/abst/firewire.nm index f1b30837..b1a87d7b 100644 --- a/prism-examples/firewire/abst/firewire.nm +++ b/prism-examples/firewire/abst/firewire.nm @@ -2,59 +2,76 @@ // gxn 23/05/2001 mdp + +// wire delay +const int delay; + +// probability of choosing fast and slow +const double fast; +const double slow = 1-fast; // largest constant the clock of the system is compared to const int kx = 167; -module abstract_firewire - - // clock of the system - x : [0..168]; - - // local state - s : [0..9]; - // 0 - start_start - // 1 - fast_start - // 2 - start_fast - // 3 - start_slow - // 4 - slow_start - // 5 - fast_fast - // 6 - fast_slow - // 7 - slow_fast - // 8 - slow_slow - // 9 - done - - // initial state - [] (s=0) & (x<36) -> (x'=min(x+1,kx+1)); - [] (s=0) -> 0.5 : (s'=1) + 0.5 : (s'=4); - [] (s=0) -> 0.5 : (s'=2) + 0.5 : (s'=3); - // fast_start - [] (s=1) & (x<36) -> (x'=min(x+1,kx+1)); - [] (s=1) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=6) & (x'=0); - // start_fast - [] (s=2) & (x<36) -> (x'=min(x+1,kx+1)); - [] (s=2) -> 0.5 : (s'=5) & (x'=0) + 0.5 : (s'=7) & (x'=0); - // start_slow - [] (s=3) & (x<36) -> (x'=min(x+1,kx+1)); - [] (s=3) -> 0.5 : (s'=6) & (x'=0) + 0.5 : (s'=8) & (x'=0); - // slow_start - [] (s=4) & (x<36) -> (x'=min(x+1,kx+1)); - [] (s=4) -> 0.5 : (s'=7) & (x'=0) + 0.5 : (s'=8) & (x'=0); - // fast_fast - [] (s=5) & (x<85) -> (x'=min(x+1,kx+1)); - [] (s=5) & (x>=76) -> (s'=0) & (x'=0); - [] (s=5) & (x>=40) -> (s'=9) & (x'=0); - // fast_slow - [] (s=6) & (x<167) -> (x'=min(x+1,kx+1)); - [] (s=6) & (x>=123) -> (s'=9) & (x'=0); - // slow_fast - [] (s=7) & (x<167) -> (x'=min(x+1,kx+1)); - [] (s=7) & (x>=123) -> (s'=9) & (x'=0); - // slow_slow - [] (s=8) & (x<167) -> (x'=min(x+1,kx+1)); - [] (s=8) & (x>=159) -> (s'=0) & (x'=0); - [] (s=8) & (x>=123) -> (s'=9) & (x'=0); - // done - [] (s=9) -> (s'=9); - -endmodule +module abstract_firewire + + // clock + x : [0..kx+1]; + + // local state + s : [0..9]; + // 0 -start_start + // 1 -fast_start + // 2 -start_fast + // 3 -start_slow + // 4 -slow_start + // 5 -fast_fast + // 6 -fast_slow + // 7 -slow_fast + // 8 -slow_slow + // 9 -done + + // initial state + [time] s=0 & x (x'=min(x+1,kx+1)); + [round] s=0 -> fast : (s'=1) + slow : (s'=4); + [round] s=0 -> fast : (s'=2) + slow : (s'=3); + // fast_start + [time] s=1 & x (x'=min(x+1,kx+1)); + [] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0); + // start_fast + [time] s=2 & x (x'=min(x+1,kx+1)); + [] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0); + // start_slow + [time] s=3 & x (x'=min(x+1,kx+1)); + [] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0); + // slow_start + [time] s=4 & x (x'=min(x+1,kx+1)); + [] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0); + // fast_fast + [time] s=5 & (x<85) -> (x'=min(x+1,kx+1)); + [] s=5 & (x>=76) -> (s'=0) & (x'=0); + [] s=5 & (x>=76-delay) -> (s'=9) & (x'=0); + // fast_slow + [time] s=6 & x<167 -> (x'=min(x+1,kx+1)); + [] s=6 & x>=159-delay -> (s'=9) & (x'=0); + // slow_fast + [time] s=7 & x<167 -> (x'=min(x+1,kx+1)); + [] s=7 & x>=159-delay -> (s'=9) & (x'=0); + // slow_slow + [time] s=8 & x<167 -> (x'=min(x+1,kx+1)); + [] s=8 & x>=159 -> (s'=0) & (x'=0); + [] s=8 & x>=159-delay -> (s'=9) & (x'=0); + // done + [] s=9 -> (s'=s); + +endmodule + +//reward structures +// time +rewards "time" + [time] true : 1; +endrewards +// number of rounds +rewards "rounds" + [round] true : 1; +endrewards