From 4630195d596d0c9e94b5f8115761ab897a3f1a51 Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Fri, 5 Dec 2008 12:08:35 +0000 Subject: [PATCH] expected properties for impl version of firewire git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@851 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/firewire/impl/auto | 13 +- prism-examples/firewire/impl/firewire.nm | 317 ++++++++++++----------- 2 files changed, 178 insertions(+), 152 deletions(-) diff --git a/prism-examples/firewire/impl/auto b/prism-examples/firewire/impl/auto index f9f807cd..97b35868 100755 --- a/prism-examples/firewire/impl/auto +++ b/prism-examples/firewire/impl/auto @@ -1,9 +1,18 @@ #!/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=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 sending +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) - 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/impl/firewire.nm b/prism-examples/firewire/impl/firewire.nm index 1349d70d..db364755 100644 --- a/prism-examples/firewire/impl/firewire.nm +++ b/prism-examples/firewire/impl/firewire.nm @@ -1,150 +1,167 @@ -// full firewire protocol with integer semantics -// dxp/gxn 14/06/01 - -// CLOCKS -// x1 clock for node1 -// x2 clock for node2 -// y1 and y2 clocks for wire12 -// z1 and z2 clocks for wire21 - -// maximum and minimum delays -// for fast -const int rc_fast_max = 85; -const int rc_fast_min = 76; -// for slow -const int rc_slow_max = 167; -const int rc_slow_min = 159; -// for wire -const int delay = 36; - -module wire12 - - // local state - w12 : [0..9]; - // 0 - empty - // 1 - rec_req - // 2 - rec_req_ack - // 3 - rec_ack - // 4 - rec_ack_idle - // 5 - rec_idle - // 6 - rec_idle_req - // 7 - rec_ack_req - // 8 - rec_req_idle - // 9 - rec_idle_ack - - // clocks for wire12 - y1 : [0..37]; - y2 : [0..37]; - - // empty - // do not need y1 and y2 to increase as always reset when this state is left - // similarly can reset y1 and y2 when we re-enter this state - [snd_req12] (w12=0) -> (w12'=1) & (y1'=0) & (y2'=0); - [snd_ack12] (w12=0) -> (w12'=3) & (y1'=0) & (y2'=0); - [snd_idle12] (w12=0) -> (w12'=5) & (y1'=0) & (y2'=0); - [time] (w12=0) -> (w12'=w12); - // rec_req - [snd_req12] (w12=1) -> (w12'=1); - [rec_req12] (w12=1) -> (w12'=0) & (y1'=0) & (y2'=0); - [snd_ack12] (w12=1) -> (w12'=2) & (y2'=0); - [snd_idle12] (w12=1) -> (w12'=8) & (y2'=0); - [time] (w12=1) & (y2 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_req_ack - [snd_ack12] (w12=2) -> (w12'=2); - [rec_req12] (w12=2) -> (w12'=3); - [time] (w12=2) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_ack - [snd_ack12] (w12=3) -> (w12'=3); - [rec_ack12] (w12=3) -> (w12'=0) & (y1'=0) & (y2'=0); - [snd_idle12] (w12=3) -> (w12'=4) & (y2'=0); - [snd_req12] (w12=3) -> (w12'=7) & (y2'=0); - [time] (w12=3) & (y2 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_ack_idle - [snd_idle12] (w12=4) -> (w12'=4); - [rec_ack12] (w12=4) -> (w12'=5); - [time] (w12=4) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_idle - [snd_idle12] (w12=5) -> (w12'=5); - [rec_idle12] (w12=5) -> (w12'=0) & (y1'=0) & (y2'=0); - [snd_req12] (w12=5) -> (w12'=6) & (y2'=0); - [snd_ack12] (w12=5) -> (w12'=9) & (y2'=0); - [time] (w12=5) & (y2 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_idle_req - [snd_req12] (w12=6) -> (w12'=6); - [rec_idle12] (w12=6) -> (w12'=1); - [time] (w12=6) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_ack_req - [snd_req12] (w12=7) -> (w12'=7); - [rec_ack12] (w12=7) -> (w12'=1); - [time] (w12=7) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_req_idle - [snd_idle12] (w12=8) -> (w12'=8); - [rec_req12] (w12=8) -> (w12'=5); - [time] (w12=8) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - // rec_idle_ack - [snd_ack12] (w12=9) -> (w12'=9); - [rec_idle12] (w12=9) -> (w12'=3); - [time] (w12=9) & (y1 (y1'=min(y1+1,37)) & (y2'=min(y2+1,37)); - -endmodule - -module node1 - - // clock for node1 - x1 : [0..168]; - // local state - s1 : [0..8]; - // 0 - root contention - // 1 - rec_idle - // 2 - rec_req_fast - // 3 - rec_req_slow - // 4 - rec_idle_fast - // 5 - rec_idle_slow - // 6 - snd_req - // 7- almost_root - // 8 - almost_child - // added resets to x1 when not considered again until after rest - // removed root and child (using almost root and almost child) - - // root contention (immediate state) - [snd_idle12] (s1=0) -> 0.5 : (s1'=2) & (x1'=0) + 0.5 : (s1'=3) & (x1'=0); - [rec_idle21] (s1=0) -> (s1'=1); - // rec_idle (immediate state) - [snd_idle12] (s1=1) -> 0.5 : (s1'=4) & (x1'=0) + 0.5 : (s1'=5) & (x1'=0); - [rec_req21] (s1=1) -> (s1'=0); - // rec_req_fast - [rec_idle21] (s1=2) -> (s1'=4); - [snd_ack12] (s1=2) & (x1>=rc_fast_min) -> (s1'=7) & (x1'=0); - [time] (s1=2) & (x1 (x1'=min(x1+1,168)); - // rec_req_slow - [rec_idle21] (s1=3) -> (s1'=5); - [snd_ack12] (s1=3) & (x1>=rc_slow_min) -> (s1'=7) & (x1'=0); - [time] (s1=3) & (x1 (x1'=min(x1+1,168)); - // rec_idle_fast - [rec_req21] (s1=4) -> (s1'=2); - [snd_req12] (s1=4) & (x1>=rc_fast_min) -> (s1'=6) & (x1'=0); - [time] (s1=4) & (x1 (x1'=min(x1+1,168)); - // rec_idle_slow - [rec_req21] (s1=5) -> (s1'=3); - [snd_req12] (s1=5) & (x1>=rc_slow_min) -> (s1'=6) & (x1'=0); - [time] (s1=5) & (x1 (x1'=min(x1+1,168)); - // snd_req - // do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 - // also can set x1 to 0 upon entering this state - [rec_req21] (s1=6) -> (s1'=0); - [rec_ack21] (s1=6) -> (s1'=8); - [time] (s1=6) -> (s1'=s1); - // loop in final states to remove deadlock (but wait until both process have decided) - [] (s1=7) & (s2=8) -> (s1'=s1); - [time] (s1=7) -> (s1'=s1); - -endmodule - -// wire21 -module wire21=wire12[w12=w21, y1=z1, y2=z2, snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, - rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] endmodule - -// node2 -module node2=node1[s1=s2, s2=s1, x1=x2, rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, - snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] endmodule - +// firewire protocol with integer semantics +// dxp/gxn 14/06/01 + +// CLOCKS +// x1 (x2) clock for node1 (node2) +// y1 and y2 (z1 and z2) clocks for wire12 (wire21) + +// maximum and minimum delays +// fast +const int rc_fast_max = 85; +const int rc_fast_min = 76; +// slow +const int rc_slow_max = 167; +const int rc_slow_min = 159; +// delay caused by the wire length +const int delay; +// probability of choosing fast +const double fast; +const double slow=1-fast; + +module wire12 + + // local state + w12 : [0..9]; + // 0 - empty + // 1 - rec_req + // 2 - rec_req_ack + // 3 - rec_ack + // 4 - rec_ack_idle + // 5 - rec_idle + // 6 - rec_idle_req + // 7 - rec_ack_req + // 8 - rec_req_idle + // 9 - rec_idle_ack + + // clock for wire12 + y1 : [0..delay+1]; + y2 : [0..delay+1]; + + // empty + // do not need y1 and y2 to increase as always reset when this state is left + // similarly can reset y1 and y2 when we re-enter this state + [snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); + [snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); + [snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); + [time] w12=0 -> (w12'=w12); + // rec_req + [snd_req12] w12=1 -> (w12'=1); + [rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_ack12] w12=1 -> (w12'=2) & (y2'=0); + [snd_idle12] w12=1 -> (w12'=8) & (y2'=0); + [time] w12=1 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_ack + [snd_ack12] w12=2 -> (w12'=2); + [rec_req12] w12=2 -> (w12'=3); + [time] w12=2 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack + [snd_ack12] w12=3 -> (w12'=3); + [rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_idle12] w12=3 -> (w12'=4) & (y2'=0); + [snd_req12] w12=3 -> (w12'=7) & (y2'=0); + [time] w12=3 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_idle + [snd_idle12] w12=4 -> (w12'=4); + [rec_ack12] w12=4 -> (w12'=5); + [time] w12=4 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle + [snd_idle12] w12=5 -> (w12'=5); + [rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_req12] w12=5 -> (w12'=6) & (y2'=0); + [snd_ack12] w12=5 -> (w12'=9) & (y2'=0); + [time] w12=5 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_req + [snd_req12] w12=6 -> (w12'=6); + [rec_idle12] w12=6 -> (w12'=1); + [time] w12=6 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_req + [snd_req12] w12=7 -> (w12'=7); + [rec_ack12] w12=7 -> (w12'=1); + [time] w12=7 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_idle + [snd_idle12] w12=8 -> (w12'=8); + [rec_req12] w12=8 -> (w12'=5); + [time] w12=8 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_ack + [snd_ack12] w12=9 -> (w12'=9); + [rec_idle12] w12=9 -> (w12'=3); + [time] w12=9 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + +endmodule + +module node1 + + // clock for node1 + x1 : [0..168]; + + // local state + s1 : [0..8]; + // 0 - root contention + // 1 - rec_idle + // 2 - rec_req_fast + // 3 - rec_req_slow + // 4 - rec_idle_fast + // 5 - rec_idle_slow + // 6 - snd_req + // 7- almost_root + // 8 - almost_child + + // added resets to x1 when not considered again until after rest + // removed root and child (using almost root and almost child) + + // root contention immediate state) + [snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); + [rec_idle21] s1=0 -> (s1'=1); + // rec_idle immediate state) + [snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); + [rec_req21] s1=1 -> (s1'=0); + // rec_req_fast + [rec_idle21] s1=2 -> (s1'=4); + [snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); + [time] s1=2 & x1 (x1'=min(x1+1,168)); + // rec_req_slow + [rec_idle21] s1=3 -> (s1'=5); + [snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); + [time] s1=3 & x1 (x1'=min(x1+1,168)); + // rec_idle_fast + [rec_req21] s1=4 -> (s1'=2); + [snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); + [time] s1=4 & x1 (x1'=min(x1+1,168)); + // rec_idle_slow + [rec_req21] s1=5 -> (s1'=3); + [snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); + [time] s1=5 & x1 (x1'=min(x1+1,168)); + // snd_req + // do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 + // also can set x1 to 0 upon entering this state + [rec_req21] s1=6 -> (s1'=0); + [rec_ack21] s1=6 -> (s1'=8); + [time] s1=6 -> (s1'=s1); + // almost root (immediate) + // loop in final states to remove deadlock + [] s1=7 & s2=8 -> (s1'=s1); + [] s1=8 & s2=7 -> (s1'=s1); + [time] s1=7 -> (s1'=s1); + [time] s1=8 -> (s1'=s1); + +endmodule + +// construct remaining automata through renaming +module wire21=wire12[w12=w21, y1=z1, y2=z2, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, + rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] +endmodule +module node2=node1[s1=s2, s2=s1, x1=x2, + rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] +endmodule + +// reward structures +// time +rewards "time" + [time] true : 1; +endrewards +// time nodes sending +rewards "time_sending" + [time] (w12>0 | w21>0) : 1; +endrewards