TimQu
9 years ago
8 changed files with 955 additions and 8 deletions
-
6examples/pmdp/firewire/firewire.prop
-
2examples/pmdp/firewire/firewire_3.pm
-
176examples/pmdp/firewire/firewire_36.pm
-
3examples/pmdp/zeroconf/zeroconf.prop
-
2examples/pmdp/zeroconf/zeroconf_2.nm
-
258examples/pmdp/zeroconf/zeroconf_4.nm
-
258examples/pmdp/zeroconf/zeroconf_6.nm
-
258examples/pmdp/zeroconf/zeroconf_8.nm
@ -1,4 +1,2 @@ |
|||
Pmin=?[ F (s1=8 & s2=7) ] |
|||
//R{"time"}min=? [ F "done" ] |
|||
//R{"time"}max=? [ F "done" ] |
|||
//R{"time_sending"}max=? [ F "done" ] |
|||
P>0.5[ F (s1=7 & s2=8) ] |
|||
|
|||
@ -0,0 +1,176 @@ |
|||
// 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=36; |
|||
// probability of choosing fast |
|||
const double fast1; // = 0.5; |
|||
const double slow1=1-fast1; |
|||
const double fast2; // = 0.5; |
|||
const double slow2=1-fast2; |
|||
|
|||
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 -> fast1 : (s1'=2) & (x1'=0) + slow1 : (s1'=3) & (x1'=0); |
|||
[rec_idle21] s1=0 -> (s1'=1); |
|||
// rec_idle immediate state) |
|||
[snd_idle12] s1=1 -> fast1 : (s1'=4) & (x1'=0) + slow1 : (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, fast1=fast2, slow1=slow2, |
|||
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 |
|||
|
|||
// labels |
|||
label "done" = (s1=8 & s2=7) | (s1=7 & s2=8); |
|||
|
|||
// reward structures |
|||
|
|||
// time |
|||
rewards "time" |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
// time nodes sending |
|||
rewards "time_sending" |
|||
[time] (w12>0 | w21>0) : 1; |
|||
endrewards |
|||
@ -1,2 +1 @@ |
|||
Pmin=? [ F (l=4 & ip=1) ] |
|||
Pmax=? [ F (l=4 & ip=1) ] |
|||
P<=0.1 [ F (l=4 & ip=1) ] |
|||
@ -0,0 +1,258 @@ |
|||
// IPv4: PTA model with digitial clocks |
|||
// one concrete host attempting to choose an ip address |
|||
// when a number of (abstract) hosts have already got ip addresses |
|||
// gxn/dxp/jzs 02/05/03 |
|||
|
|||
// model is an mdp |
|||
mdp |
|||
|
|||
// reset or noreset model |
|||
const bool reset=false; |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
// we suppose that |
|||
// - the abstract hosts have already picked their addresses |
|||
// and always defend their addresses |
|||
// - the concrete host never picks the same ip address twice |
|||
// (this can happen only with a verys small probability) |
|||
|
|||
// under these assumptions we do not need message types because: |
|||
// 1) since messages to the concrete host will never be a probe, |
|||
// this host will react to all messages in the same way |
|||
// 2) since the abstract hosts always defend their addresses, |
|||
// all messages from the host will get an arp reply if the ip matches |
|||
|
|||
// following from the above assumptions we require only three abstract IP addresses |
|||
// (0,1 and 2) which correspond to the following sets of IP addresses: |
|||
|
|||
// 0 - the IP addresses of the abstract hosts which the concrete host |
|||
// previously tried to configure |
|||
// 1 - an IP address of an abstract host which the concrete host is |
|||
// currently trying to configure |
|||
// 2 - a fresh IP address which the concrete host is currently trying to configure |
|||
|
|||
// if the host picks an address that is being used it may end up picking another ip address |
|||
// in which case there may still be messages corresponding to the old ip address |
|||
// to be sent both from and to the host which the host should now disregard |
|||
// (since it will never pick the same ip address) |
|||
|
|||
// to deal with this situation: when a host picks a new ip address we reconfigure the |
|||
// messages that are still be be sent or are being sent by changing the ip address to 0 |
|||
// (an old ip address of the host) |
|||
|
|||
// all the messages from the abstract hosts for the 'old' address (in fact the |
|||
// set of old addresses since it may have started again more than once) |
|||
// can arrive in any order since they are equivalent to the host - it ignores then all |
|||
|
|||
// also the messages for the old and new address will come from different hosts |
|||
// (the ones with that ip address) which we model by allowing them to arrive in any order |
|||
// i.e. not neccessarily in the order they where sent |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
|
|||
//------------------------------------------------------------- |
|||
// VARIABLES |
|||
//const int N; // number of abstract hosts |
|||
const int K=4; // number of probes to send |
|||
const double loss; // probability of message loss |
|||
|
|||
// PROBABILITIES |
|||
const double old; //=N/65024; // probability pick an ip address being used |
|||
const double new = (1-old); // probability pick a new ip address |
|||
|
|||
// TIMING CONSTANTS |
|||
const int CONSEC = 2; // time interval between sending consecutive probles |
|||
const int TRANSTIME = 1; // upper bound on transmission time delay |
|||
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions |
|||
const int DEFEND = 10; |
|||
|
|||
const int TIME_MAX_X = 60; // max value of clock x |
|||
const int TIME_MAX_Y = 10; // max value of clock y |
|||
const int TIME_MAX_Z = 1; // max value of clock z |
|||
|
|||
// OTHER CONSTANTS |
|||
const int MAXCOLL = 10; // maximum number of collisions before long wait |
|||
// size of buffers for other hosts |
|||
const int B0 = 20; // buffer size for one abstract host |
|||
const int B1 = 8; // buffer sizes for all abstract hosts |
|||
|
|||
//------------------------------------------------------------- |
|||
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts |
|||
module environment |
|||
|
|||
// buffer of concrete host |
|||
b_ip7 : [0..2]; // ip address of message in buffer position 8 |
|||
b_ip6 : [0..2]; // ip address of message in buffer position 7 |
|||
b_ip5 : [0..2]; // ip address of message in buffer position 6 |
|||
b_ip4 : [0..2]; // ip address of message in buffer position 5 |
|||
b_ip3 : [0..2]; // ip address of message in buffer position 4 |
|||
b_ip2 : [0..2]; // ip address of message in buffer position 3 |
|||
b_ip1 : [0..2]; // ip address of message in buffer position 2 |
|||
b_ip0 : [0..2]; // ip address of message in buffer position 1 |
|||
n : [0..8]; // number of places in the buffer used (from host) |
|||
|
|||
// messages to be sent from abstract hosts to concrete host |
|||
n0 : [0..B0]; // number of messages which do not have the host's current ip address |
|||
n1 : [0..B1]; // number of messages which have the host's current ip address |
|||
|
|||
b : [0..2]; // local state |
|||
// 0 - idle |
|||
// 1 - sending message from concrete host |
|||
// 2 - sending message from abstract host |
|||
|
|||
z : [0..1]; // clock of environment (needed for the time to send a message) |
|||
|
|||
ip_mess : [0..2]; // ip in the current message being sent |
|||
// 0 - different from concrete host |
|||
// 1 - same as the concrete host and in use |
|||
// 2 - same as the concrete host and not in use |
|||
|
|||
// RESET/RECONFIG: when host is about to choose new ip address |
|||
// suppose that the host cannot choose the same ip address |
|||
// (since happens with very small probability). |
|||
// Therefore all messages will have a different ip address, |
|||
// i.e. all n1 messages become n0 ones. |
|||
// Note this include any message currently being sent (ip is set to zero 0) |
|||
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers |
|||
& (ip_mess'=0) // message being set |
|||
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=0) |
|||
& (b_ip5'=0) |
|||
& (b_ip4'=0) |
|||
& (b_ip3'=0) |
|||
& (b_ip2'=0) |
|||
& (b_ip1'=0) |
|||
& (b_ip0'=0); |
|||
// note: prevent anything else from happening when reconfiguration needs to take place |
|||
|
|||
// time passage (only if no messages to send or sending a message) |
|||
[time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message |
|||
[time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message |
|||
|
|||
// get messages to be sent (so message has same ip address as host) |
|||
[send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1); |
|||
[send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1); |
|||
[send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1); |
|||
[send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1); |
|||
[send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1); |
|||
[send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1); |
|||
[send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1); |
|||
[send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1); |
|||
[send] l>0 & n=8 -> (n'=n); // buffer full so lose message |
|||
|
|||
// start sending message from host |
|||
[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) |
|||
& (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1) // send message |
|||
+ loss : (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1); // lose message |
|||
|
|||
// start sending message to host |
|||
[] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip |
|||
[] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip |
|||
|
|||
// finish sending message from host |
|||
[] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
// finish sending message to host |
|||
[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
endmodule |
|||
|
|||
//------------------------------------------------------------- |
|||
// CONCRETE HOST |
|||
module host0 |
|||
|
|||
x : [0..TIME_MAX_X]; // first clock of the host |
|||
y : [0..TIME_MAX_Y]; // second clock of the host |
|||
|
|||
coll : [0..MAXCOLL]; // number of address collisions |
|||
probes : [0..K]; // counter (number of probes sent) |
|||
mess : [0..1]; // need to send a message or not |
|||
defend : [0..1]; // defend (if =1, try to defend IP address) |
|||
|
|||
ip : [1..2]; // ip address (1 - in use & 2 - fresh) |
|||
|
|||
l : [0..4] init 1; // location |
|||
// 0 : RECONFIGURE |
|||
// 1 : RANDOM |
|||
// 2 : WAITSP |
|||
// 3 : WAITSG |
|||
// 4 : USE |
|||
|
|||
// RECONFIGURE |
|||
[reset] l=0 -> (l'=1); |
|||
|
|||
// RANDOM (choose IP address) |
|||
[rec] (l=1) -> 1: true; // get message (ignore since have no ip address) |
|||
// small number of collisions (choose straight away) |
|||
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
// large number of collisions: (wait for LONGWAIT) |
|||
[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X)); |
|||
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
|
|||
// WAITSP |
|||
// let time pass |
|||
[time] l=2 & x<2 -> (x'=min(x+1,2)); |
|||
// send probe |
|||
[send] l=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1); |
|||
// sent K probes and waited 2 seconds |
|||
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0); |
|||
// get message and ip does not match: ignore |
|||
[rec] l=2 & ip_mess!=ip -> (l'=l); |
|||
// get a message with matching ip: reconfigure |
|||
[rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0); |
|||
|
|||
// WAITSG (sends two gratuitious arp probes) |
|||
// time passage |
|||
[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); |
|||
[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND)); |
|||
|
|||
// receive message and same ip: defend |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0); |
|||
// receive message and same ip: defer |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0); |
|||
// receive message and different ip |
|||
[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l); |
|||
|
|||
|
|||
// send probe reply or message for defence |
|||
[send] l=3 & mess=1 -> (mess'=0); |
|||
// send first gratuitous arp message |
|||
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1); |
|||
// send second gratuitous arp message (move to use) |
|||
[send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0); |
|||
|
|||
// USE (only interested in reaching this state so do not need to add anything here) |
|||
[] l=4 -> 1 : true; |
|||
|
|||
endmodule |
|||
@ -0,0 +1,258 @@ |
|||
// IPv4: PTA model with digitial clocks |
|||
// one concrete host attempting to choose an ip address |
|||
// when a number of (abstract) hosts have already got ip addresses |
|||
// gxn/dxp/jzs 02/05/03 |
|||
|
|||
// model is an mdp |
|||
mdp |
|||
|
|||
// reset or noreset model |
|||
const bool reset=false; |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
// we suppose that |
|||
// - the abstract hosts have already picked their addresses |
|||
// and always defend their addresses |
|||
// - the concrete host never picks the same ip address twice |
|||
// (this can happen only with a verys small probability) |
|||
|
|||
// under these assumptions we do not need message types because: |
|||
// 1) since messages to the concrete host will never be a probe, |
|||
// this host will react to all messages in the same way |
|||
// 2) since the abstract hosts always defend their addresses, |
|||
// all messages from the host will get an arp reply if the ip matches |
|||
|
|||
// following from the above assumptions we require only three abstract IP addresses |
|||
// (0,1 and 2) which correspond to the following sets of IP addresses: |
|||
|
|||
// 0 - the IP addresses of the abstract hosts which the concrete host |
|||
// previously tried to configure |
|||
// 1 - an IP address of an abstract host which the concrete host is |
|||
// currently trying to configure |
|||
// 2 - a fresh IP address which the concrete host is currently trying to configure |
|||
|
|||
// if the host picks an address that is being used it may end up picking another ip address |
|||
// in which case there may still be messages corresponding to the old ip address |
|||
// to be sent both from and to the host which the host should now disregard |
|||
// (since it will never pick the same ip address) |
|||
|
|||
// to deal with this situation: when a host picks a new ip address we reconfigure the |
|||
// messages that are still be be sent or are being sent by changing the ip address to 0 |
|||
// (an old ip address of the host) |
|||
|
|||
// all the messages from the abstract hosts for the 'old' address (in fact the |
|||
// set of old addresses since it may have started again more than once) |
|||
// can arrive in any order since they are equivalent to the host - it ignores then all |
|||
|
|||
// also the messages for the old and new address will come from different hosts |
|||
// (the ones with that ip address) which we model by allowing them to arrive in any order |
|||
// i.e. not neccessarily in the order they where sent |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
|
|||
//------------------------------------------------------------- |
|||
// VARIABLES |
|||
//const int N; // number of abstract hosts |
|||
const int K=6; // number of probes to send |
|||
const double loss; // probability of message loss |
|||
|
|||
// PROBABILITIES |
|||
const double old; //=N/65024; // probability pick an ip address being used |
|||
const double new = (1-old); // probability pick a new ip address |
|||
|
|||
// TIMING CONSTANTS |
|||
const int CONSEC = 2; // time interval between sending consecutive probles |
|||
const int TRANSTIME = 1; // upper bound on transmission time delay |
|||
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions |
|||
const int DEFEND = 10; |
|||
|
|||
const int TIME_MAX_X = 60; // max value of clock x |
|||
const int TIME_MAX_Y = 10; // max value of clock y |
|||
const int TIME_MAX_Z = 1; // max value of clock z |
|||
|
|||
// OTHER CONSTANTS |
|||
const int MAXCOLL = 10; // maximum number of collisions before long wait |
|||
// size of buffers for other hosts |
|||
const int B0 = 20; // buffer size for one abstract host |
|||
const int B1 = 8; // buffer sizes for all abstract hosts |
|||
|
|||
//------------------------------------------------------------- |
|||
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts |
|||
module environment |
|||
|
|||
// buffer of concrete host |
|||
b_ip7 : [0..2]; // ip address of message in buffer position 8 |
|||
b_ip6 : [0..2]; // ip address of message in buffer position 7 |
|||
b_ip5 : [0..2]; // ip address of message in buffer position 6 |
|||
b_ip4 : [0..2]; // ip address of message in buffer position 5 |
|||
b_ip3 : [0..2]; // ip address of message in buffer position 4 |
|||
b_ip2 : [0..2]; // ip address of message in buffer position 3 |
|||
b_ip1 : [0..2]; // ip address of message in buffer position 2 |
|||
b_ip0 : [0..2]; // ip address of message in buffer position 1 |
|||
n : [0..8]; // number of places in the buffer used (from host) |
|||
|
|||
// messages to be sent from abstract hosts to concrete host |
|||
n0 : [0..B0]; // number of messages which do not have the host's current ip address |
|||
n1 : [0..B1]; // number of messages which have the host's current ip address |
|||
|
|||
b : [0..2]; // local state |
|||
// 0 - idle |
|||
// 1 - sending message from concrete host |
|||
// 2 - sending message from abstract host |
|||
|
|||
z : [0..1]; // clock of environment (needed for the time to send a message) |
|||
|
|||
ip_mess : [0..2]; // ip in the current message being sent |
|||
// 0 - different from concrete host |
|||
// 1 - same as the concrete host and in use |
|||
// 2 - same as the concrete host and not in use |
|||
|
|||
// RESET/RECONFIG: when host is about to choose new ip address |
|||
// suppose that the host cannot choose the same ip address |
|||
// (since happens with very small probability). |
|||
// Therefore all messages will have a different ip address, |
|||
// i.e. all n1 messages become n0 ones. |
|||
// Note this include any message currently being sent (ip is set to zero 0) |
|||
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers |
|||
& (ip_mess'=0) // message being set |
|||
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=0) |
|||
& (b_ip5'=0) |
|||
& (b_ip4'=0) |
|||
& (b_ip3'=0) |
|||
& (b_ip2'=0) |
|||
& (b_ip1'=0) |
|||
& (b_ip0'=0); |
|||
// note: prevent anything else from happening when reconfiguration needs to take place |
|||
|
|||
// time passage (only if no messages to send or sending a message) |
|||
[time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message |
|||
[time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message |
|||
|
|||
// get messages to be sent (so message has same ip address as host) |
|||
[send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1); |
|||
[send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1); |
|||
[send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1); |
|||
[send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1); |
|||
[send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1); |
|||
[send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1); |
|||
[send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1); |
|||
[send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1); |
|||
[send] l>0 & n=8 -> (n'=n); // buffer full so lose message |
|||
|
|||
// start sending message from host |
|||
[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) |
|||
& (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1) // send message |
|||
+ loss : (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1); // lose message |
|||
|
|||
// start sending message to host |
|||
[] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip |
|||
[] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip |
|||
|
|||
// finish sending message from host |
|||
[] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
// finish sending message to host |
|||
[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
endmodule |
|||
|
|||
//------------------------------------------------------------- |
|||
// CONCRETE HOST |
|||
module host0 |
|||
|
|||
x : [0..TIME_MAX_X]; // first clock of the host |
|||
y : [0..TIME_MAX_Y]; // second clock of the host |
|||
|
|||
coll : [0..MAXCOLL]; // number of address collisions |
|||
probes : [0..K]; // counter (number of probes sent) |
|||
mess : [0..1]; // need to send a message or not |
|||
defend : [0..1]; // defend (if =1, try to defend IP address) |
|||
|
|||
ip : [1..2]; // ip address (1 - in use & 2 - fresh) |
|||
|
|||
l : [0..4] init 1; // location |
|||
// 0 : RECONFIGURE |
|||
// 1 : RANDOM |
|||
// 2 : WAITSP |
|||
// 3 : WAITSG |
|||
// 4 : USE |
|||
|
|||
// RECONFIGURE |
|||
[reset] l=0 -> (l'=1); |
|||
|
|||
// RANDOM (choose IP address) |
|||
[rec] (l=1) -> 1: true; // get message (ignore since have no ip address) |
|||
// small number of collisions (choose straight away) |
|||
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
// large number of collisions: (wait for LONGWAIT) |
|||
[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X)); |
|||
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
|
|||
// WAITSP |
|||
// let time pass |
|||
[time] l=2 & x<2 -> (x'=min(x+1,2)); |
|||
// send probe |
|||
[send] l=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1); |
|||
// sent K probes and waited 2 seconds |
|||
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0); |
|||
// get message and ip does not match: ignore |
|||
[rec] l=2 & ip_mess!=ip -> (l'=l); |
|||
// get a message with matching ip: reconfigure |
|||
[rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0); |
|||
|
|||
// WAITSG (sends two gratuitious arp probes) |
|||
// time passage |
|||
[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); |
|||
[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND)); |
|||
|
|||
// receive message and same ip: defend |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0); |
|||
// receive message and same ip: defer |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0); |
|||
// receive message and different ip |
|||
[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l); |
|||
|
|||
|
|||
// send probe reply or message for defence |
|||
[send] l=3 & mess=1 -> (mess'=0); |
|||
// send first gratuitous arp message |
|||
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1); |
|||
// send second gratuitous arp message (move to use) |
|||
[send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0); |
|||
|
|||
// USE (only interested in reaching this state so do not need to add anything here) |
|||
[] l=4 -> 1 : true; |
|||
|
|||
endmodule |
|||
@ -0,0 +1,258 @@ |
|||
// IPv4: PTA model with digitial clocks |
|||
// one concrete host attempting to choose an ip address |
|||
// when a number of (abstract) hosts have already got ip addresses |
|||
// gxn/dxp/jzs 02/05/03 |
|||
|
|||
// model is an mdp |
|||
mdp |
|||
|
|||
// reset or noreset model |
|||
const bool reset=false; |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
// we suppose that |
|||
// - the abstract hosts have already picked their addresses |
|||
// and always defend their addresses |
|||
// - the concrete host never picks the same ip address twice |
|||
// (this can happen only with a verys small probability) |
|||
|
|||
// under these assumptions we do not need message types because: |
|||
// 1) since messages to the concrete host will never be a probe, |
|||
// this host will react to all messages in the same way |
|||
// 2) since the abstract hosts always defend their addresses, |
|||
// all messages from the host will get an arp reply if the ip matches |
|||
|
|||
// following from the above assumptions we require only three abstract IP addresses |
|||
// (0,1 and 2) which correspond to the following sets of IP addresses: |
|||
|
|||
// 0 - the IP addresses of the abstract hosts which the concrete host |
|||
// previously tried to configure |
|||
// 1 - an IP address of an abstract host which the concrete host is |
|||
// currently trying to configure |
|||
// 2 - a fresh IP address which the concrete host is currently trying to configure |
|||
|
|||
// if the host picks an address that is being used it may end up picking another ip address |
|||
// in which case there may still be messages corresponding to the old ip address |
|||
// to be sent both from and to the host which the host should now disregard |
|||
// (since it will never pick the same ip address) |
|||
|
|||
// to deal with this situation: when a host picks a new ip address we reconfigure the |
|||
// messages that are still be be sent or are being sent by changing the ip address to 0 |
|||
// (an old ip address of the host) |
|||
|
|||
// all the messages from the abstract hosts for the 'old' address (in fact the |
|||
// set of old addresses since it may have started again more than once) |
|||
// can arrive in any order since they are equivalent to the host - it ignores then all |
|||
|
|||
// also the messages for the old and new address will come from different hosts |
|||
// (the ones with that ip address) which we model by allowing them to arrive in any order |
|||
// i.e. not neccessarily in the order they where sent |
|||
|
|||
//------------------------------------------------------------- |
|||
|
|||
|
|||
//------------------------------------------------------------- |
|||
// VARIABLES |
|||
//const int N; // number of abstract hosts |
|||
const int K=8; // number of probes to send |
|||
const double loss; // probability of message loss |
|||
|
|||
// PROBABILITIES |
|||
const double old; //=N/65024; // probability pick an ip address being used |
|||
const double new = (1-old); // probability pick a new ip address |
|||
|
|||
// TIMING CONSTANTS |
|||
const int CONSEC = 2; // time interval between sending consecutive probles |
|||
const int TRANSTIME = 1; // upper bound on transmission time delay |
|||
const int LONGWAIT = 60; // minimum time delay after a high number of address collisions |
|||
const int DEFEND = 10; |
|||
|
|||
const int TIME_MAX_X = 60; // max value of clock x |
|||
const int TIME_MAX_Y = 10; // max value of clock y |
|||
const int TIME_MAX_Z = 1; // max value of clock z |
|||
|
|||
// OTHER CONSTANTS |
|||
const int MAXCOLL = 10; // maximum number of collisions before long wait |
|||
// size of buffers for other hosts |
|||
const int B0 = 20; // buffer size for one abstract host |
|||
const int B1 = 8; // buffer sizes for all abstract hosts |
|||
|
|||
//------------------------------------------------------------- |
|||
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts |
|||
module environment |
|||
|
|||
// buffer of concrete host |
|||
b_ip7 : [0..2]; // ip address of message in buffer position 8 |
|||
b_ip6 : [0..2]; // ip address of message in buffer position 7 |
|||
b_ip5 : [0..2]; // ip address of message in buffer position 6 |
|||
b_ip4 : [0..2]; // ip address of message in buffer position 5 |
|||
b_ip3 : [0..2]; // ip address of message in buffer position 4 |
|||
b_ip2 : [0..2]; // ip address of message in buffer position 3 |
|||
b_ip1 : [0..2]; // ip address of message in buffer position 2 |
|||
b_ip0 : [0..2]; // ip address of message in buffer position 1 |
|||
n : [0..8]; // number of places in the buffer used (from host) |
|||
|
|||
// messages to be sent from abstract hosts to concrete host |
|||
n0 : [0..B0]; // number of messages which do not have the host's current ip address |
|||
n1 : [0..B1]; // number of messages which have the host's current ip address |
|||
|
|||
b : [0..2]; // local state |
|||
// 0 - idle |
|||
// 1 - sending message from concrete host |
|||
// 2 - sending message from abstract host |
|||
|
|||
z : [0..1]; // clock of environment (needed for the time to send a message) |
|||
|
|||
ip_mess : [0..2]; // ip in the current message being sent |
|||
// 0 - different from concrete host |
|||
// 1 - same as the concrete host and in use |
|||
// 2 - same as the concrete host and not in use |
|||
|
|||
// RESET/RECONFIG: when host is about to choose new ip address |
|||
// suppose that the host cannot choose the same ip address |
|||
// (since happens with very small probability). |
|||
// Therefore all messages will have a different ip address, |
|||
// i.e. all n1 messages become n0 ones. |
|||
// Note this include any message currently being sent (ip is set to zero 0) |
|||
[reset] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers |
|||
& (ip_mess'=0) // message being set |
|||
& (n'=(reset)?0:n) // concrete buffer (remove this update to get NO_RESET model) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=0) |
|||
& (b_ip5'=0) |
|||
& (b_ip4'=0) |
|||
& (b_ip3'=0) |
|||
& (b_ip2'=0) |
|||
& (b_ip1'=0) |
|||
& (b_ip0'=0); |
|||
// note: prevent anything else from happening when reconfiguration needs to take place |
|||
|
|||
// time passage (only if no messages to send or sending a message) |
|||
[time] l>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message |
|||
[time] l>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message |
|||
|
|||
// get messages to be sent (so message has same ip address as host) |
|||
[send] l>0 & n=0 -> (b_ip0'=ip) & (n'=n+1); |
|||
[send] l>0 & n=1 -> (b_ip1'=ip) & (n'=n+1); |
|||
[send] l>0 & n=2 -> (b_ip2'=ip) & (n'=n+1); |
|||
[send] l>0 & n=3 -> (b_ip3'=ip) & (n'=n+1); |
|||
[send] l>0 & n=4 -> (b_ip4'=ip) & (n'=n+1); |
|||
[send] l>0 & n=5 -> (b_ip5'=ip) & (n'=n+1); |
|||
[send] l>0 & n=6 -> (b_ip6'=ip) & (n'=n+1); |
|||
[send] l>0 & n=7 -> (b_ip7'=ip) & (n'=n+1); |
|||
[send] l>0 & n=8 -> (n'=n); // buffer full so lose message |
|||
|
|||
// start sending message from host |
|||
[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) |
|||
& (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1) // send message |
|||
+ loss : (n'=n-1) |
|||
& (b_ip7'=0) |
|||
& (b_ip6'=b_ip7) |
|||
& (b_ip5'=b_ip6) |
|||
& (b_ip4'=b_ip5) |
|||
& (b_ip3'=b_ip4) |
|||
& (b_ip2'=b_ip3) |
|||
& (b_ip1'=b_ip2) |
|||
& (b_ip0'=b_ip1); // lose message |
|||
|
|||
// start sending message to host |
|||
[] l>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip |
|||
[] l>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip_mess'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip |
|||
|
|||
// finish sending message from host |
|||
[] l>0 & b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); |
|||
[] l>0 & b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
// finish sending message to host |
|||
[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0); |
|||
|
|||
endmodule |
|||
|
|||
//------------------------------------------------------------- |
|||
// CONCRETE HOST |
|||
module host0 |
|||
|
|||
x : [0..TIME_MAX_X]; // first clock of the host |
|||
y : [0..TIME_MAX_Y]; // second clock of the host |
|||
|
|||
coll : [0..MAXCOLL]; // number of address collisions |
|||
probes : [0..K]; // counter (number of probes sent) |
|||
mess : [0..1]; // need to send a message or not |
|||
defend : [0..1]; // defend (if =1, try to defend IP address) |
|||
|
|||
ip : [1..2]; // ip address (1 - in use & 2 - fresh) |
|||
|
|||
l : [0..4] init 1; // location |
|||
// 0 : RECONFIGURE |
|||
// 1 : RANDOM |
|||
// 2 : WAITSP |
|||
// 3 : WAITSG |
|||
// 4 : USE |
|||
|
|||
// RECONFIGURE |
|||
[reset] l=0 -> (l'=1); |
|||
|
|||
// RANDOM (choose IP address) |
|||
[rec] (l=1) -> 1: true; // get message (ignore since have no ip address) |
|||
// small number of collisions (choose straight away) |
|||
[] l=1 & coll<MAXCOLL -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
// large number of collisions: (wait for LONGWAIT) |
|||
[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X)); |
|||
[] l=1 & coll=MAXCOLL & x=LONGWAIT -> 1/3*old : (l'=2) & (ip'=1) & (x'=0) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=1) |
|||
+ 1/3*old : (l'=2) & (ip'=1) & (x'=2) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=0) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=1) |
|||
+ 1/3*new : (l'=2) & (ip'=2) & (x'=2); |
|||
|
|||
// WAITSP |
|||
// let time pass |
|||
[time] l=2 & x<2 -> (x'=min(x+1,2)); |
|||
// send probe |
|||
[send] l=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1); |
|||
// sent K probes and waited 2 seconds |
|||
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0); |
|||
// get message and ip does not match: ignore |
|||
[rec] l=2 & ip_mess!=ip -> (l'=l); |
|||
// get a message with matching ip: reconfigure |
|||
[rec] l=2 & ip_mess=ip -> (l'=0) & (coll'=min(coll+1,MAXCOLL)) & (x'=0) & (probes'=0); |
|||
|
|||
// WAITSG (sends two gratuitious arp probes) |
|||
// time passage |
|||
[time] l=3 & mess=0 & defend=0 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); |
|||
[time] l=3 & mess=0 & defend=1 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)) & (y'=min(y+1,DEFEND)); |
|||
|
|||
// receive message and same ip: defend |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0); |
|||
// receive message and same ip: defer |
|||
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0); |
|||
// receive message and different ip |
|||
[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l); |
|||
|
|||
|
|||
// send probe reply or message for defence |
|||
[send] l=3 & mess=1 -> (mess'=0); |
|||
// send first gratuitous arp message |
|||
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1); |
|||
// send second gratuitous arp message (move to use) |
|||
[send] l=3 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (y'=0) & (probes'=0); |
|||
|
|||
// USE (only interested in reaching this state so do not need to add anything here) |
|||
[] l=4 -> 1 : true; |
|||
|
|||
endmodule |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue