s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

extended deadline model 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@852 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Gethin Norman 17 years ago
parent
4630195d59
commit
987b90bc21
1 changed files with 138 additions and 134 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 272
      prism-examples/firewire/impl/deadline.nm

272
prism-examples/firewire/impl/deadline.nm
View File

@ -17,141 +17,145 @@ 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;
// wire
const int delay;
// probability of chooisng 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
// 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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<rc_fast_max) -> (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<rc_slow_max) -> (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<rc_fast_max) -> (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<rc_slow_max) -> (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
module wire12
w12 : [0..10];
// 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..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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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<delay) -> (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
// 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<rc_fast_max) -> (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<rc_slow_max) -> (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<rc_fast_max) -> (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<rc_slow_max) -> (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
// (wait until both process have decided otherwise need fairness)
[] (s1=7) & (s2=8) -> (s1'=s1);
[time] (s1=7) -> (s1'=s1);
[] (s1=8) & (s2=7) -> (s1'=s1);
[time] (s1=8) -> (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
// timer
module timer

Write Preview
Loading…
Cancel
Save