You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
170 lines
5.4 KiB
170 lines
5.4 KiB
// 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)
|
|
mdp
|
|
|
|
// 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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<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
|
|
[] 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
|
|
|
|
label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8));
|