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

fixes to zeroconf 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1317 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Gethin Norman 17 years ago
parent
c66eecb5cc
commit
5b48be904c
4 changed files with 140 additions and 142 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. 133
      prism-examples/zeroconf/zeroconf.nm
  2. 8
      prism-examples/zeroconf/zeroconf.pctl
  3. 137
      prism-examples/zeroconf/zeroconf_time_bounded.nm
  4. 4
      prism-examples/zeroconf/zeroconf_time_bounded.pctl

133
prism-examples/zeroconf/zeroconf.nm
View File

@ -8,11 +8,11 @@ const bool reset;
//-------------------------------------------------------------
// we suppose that the abstract hosts have already picked their addresses
// and always defend their addresses
// we suppose that a host never picks the same ip address twice
// (this can happen only with a verys small probability)
// 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,
@ -66,13 +66,12 @@ 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 = 2; // max value of clock x
const int TIME_MAX_Y = 60; // max value of clock y
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
@ -103,7 +102,7 @@ module environment
z : [0..1]; // clock of environment (needed for the time to send a message)
ip : [0..2]; // ip in the current message being sent
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
@ -114,8 +113,8 @@ module environment
// 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)
[reset0] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers
& (ip'=0) // message being set
[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)
@ -128,22 +127,22 @@ module environment
// 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] l0>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message
[time] l0>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // 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)
[send0] l0>0 & n=0 -> (b_ip0'=ip0) & (n'=n+1);
[send0] l0>0 & n=1 -> (b_ip1'=ip0) & (n'=n+1);
[send0] l0>0 & n=2 -> (b_ip2'=ip0) & (n'=n+1);
[send0] l0>0 & n=3 -> (b_ip3'=ip0) & (n'=n+1);
[send0] l0>0 & n=4 -> (b_ip4'=ip0) & (n'=n+1);
[send0] l0>0 & n=5 -> (b_ip5'=ip0) & (n'=n+1);
[send0] l0>0 & n=6 -> (b_ip6'=ip0) & (n'=n+1);
[send0] l0>0 & n=7 -> (b_ip7'=ip0) & (n'=n+1);
[send0] l0>0 & n=8 -> (n'=n); // buffer full so lose message
[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
[] l0>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip'=b_ip0)
[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0)
& (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
@ -164,16 +163,16 @@ module environment
& (b_ip0'=b_ip1); // lose message
// start sending message to host
[] l0>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
[] l0>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
[] 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
[] l0>0 & b=1 & ip=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip'=0);
[] l0>0 & b=1 & ip=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip'=0);
[] l0>0 & b=1 & ip=2 -> (b'=0) & (z'=0) & (ip'=0);
[] 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
[rec0] l0>0 & b=2 -> (b'=0) & (z'=0) & (ip'=0);
[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
endmodule
@ -181,17 +180,17 @@ endmodule
// CONCRETE HOST
module host0
y0 : [0..TIME_MAX_Y]; // second clock of the host
x0 : [0..TIME_MAX_X]; // clock of the host
x : [0..TIME_MAX_X]; // first clock of the host
y : [0..TIME_MAX_Y]; // second clock of the host
coll0 : [0..MAXCOLL]; // number of address collisions
probes0 : [0..K]; // counter (number of probes sent)
mess0 : [0..1]; // need to send a message or not
defend0 : [0..1]; // defend (if =1, try to defend IP address)
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)
ip0 : [1..2]; // ip address (1 - in use & 2 - fresh)
ip : [1..2]; // ip address (1 - in use & 2 - fresh)
l0 : [0..4] init 1; // location
l : [0..4] init 1; // location
// 0 : RECONFIGURE
// 1 : RANDOM
// 2 : WAITSP
@ -199,60 +198,60 @@ module host0
// 4 : USE
// RECONFIGURE
[reset0] l0=0 -> (l0'=1);
[reset] l=0 -> (l'=1);
// RANDOM (choose IP address)
[rec0] (l0=1) -> true; // get message (ignore since have no ip address)
[rec] (l=1) -> true; // get message (ignore since have no ip address)
// small number of collisions (choose straight away)
[] l0=1 & coll0<MAXCOLL -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2);
[] 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] l0=1 & coll0=MAXCOLL & y0<LONGWAIT -> (y0'=min(y0+1,TIME_MAX_Y));
[] l0=1 & coll0=MAXCOLL & y0=LONGWAIT -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2);
[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] l0=2 & y0<2 -> (y0'=min(y0+1,2));
[time] l=2 & x<2 -> (x'=min(x+1,2));
// send probe
[send0] l0=2 & y0=2 & probes0<K -> (y0'=0) & (probes0'=probes0+1);
[send] l=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
// sent K probes and waited 2 seconds
[] l0=2 & y0=2 & probes0=K -> (l0'=3) & (probes0'=0) & (coll0'=0) & (y0'=0) & (x0'=2);
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
// get message and ip does not match: ignore
[rec0] l0=2 & ip!=ip0 -> (l0'=l0);
[rec] l=2 & ip_mess!=ip -> (l'=l);
// get a message with matching ip: reconfigure
[rec0] l0=2 & ip=ip0 -> (l0'=0) & (coll0'=min(coll0+1,MAXCOLL)) & (y0'=0) & (probes0'=0);
[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] l0=3 & mess0=0 & defend0=0 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X));
[time] l0=3 & mess0=0 & defend0=1 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND));
[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
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0>=DEFEND) -> (defend0'=1) & (mess0'=1) & (y0'=0);
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
// receive message and same ip: defer
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0<DEFEND) -> (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0);
[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
[rec0] l0=3 & mess0=0 & ip!=ip0 -> (l0'=l0);
[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l);
// send probe reply or message for defence
[send0] l0=3 & mess0=1 -> (mess0'=0);
[send] l=3 & mess=1 -> (mess'=0);
// send first gratuitous arp message
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0<1 -> (x0'=0) & (probes0'=probes0+1);
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
// send second gratuitous arp message (move to use)
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 -> (l0'=4) & (x0'=0) & (y0'=0) & (probes0'=0);
[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)
[] l0=4 -> true;
[] l=4 -> true;
endmodule
@ -263,6 +262,6 @@ const double err; // cost associated with using a IP address already in use
rewards
[time] true : 1;
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 & ip0=1 : err;
[send] l=3 & mess=0 & y=CONSEC & probes=1 & ip=1 : err;
endrewards

8
prism-examples/zeroconf/zeroconf.pctl
View File

@ -1,8 +1,8 @@
// min/max probability of configuring correctly
Pmin=?[ true U (l0=4 & ip0=1) ]
Pmax=?[ true U (l0=4 & ip0=1) ]
Pmin=?[ true U (l=4 & ip=1) ]
Pmax=?[ true U (l=4 & ip=1) ]
// min/max expected cost of configuring
Rmin=?[ F l0=4 ]
Rmax=?[ F l0=4 ]
Rmin=?[ F l=4 ]
Rmax=?[ F l=4 ]

137
prism-examples/zeroconf/zeroconf_time_bounded.nm
View File

@ -2,17 +2,18 @@
// 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
// reset or noreset model
const bool reset;
const int T;
//-------------------------------------------------------------
// we suppose that the abstract hosts have already picked their addresses
// and always defend their addresses
// we suppose that a host never picks the same ip address twice
// (this can happen only with a verys small probability)
// 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,
@ -52,7 +53,6 @@ mdp
//-------------------------------------------------------------
// VARIABLES
const int T; // time bound
const int N; // number of abstract hosts
const int K; // number of probes to send
const double loss; // probability of message loss
@ -67,13 +67,12 @@ 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 = 2; // max value of clock x
const int TIME_MAX_Y = 60; // max value of clock y
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
@ -104,7 +103,7 @@ module environment
z : [0..1]; // clock of environment (needed for the time to send a message)
ip : [0..2]; // ip in the current message being sent
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
@ -115,8 +114,8 @@ module environment
// 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)
[reset0] true -> (n1'=0) & (n0'=min(B0,n0+n1)) // abstract buffers
& (ip'=0) // message being set
[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)
@ -129,22 +128,22 @@ module environment
// 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] l0>0 & b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message
[time] l0>0 & b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // 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)
[send0] l0>0 & n=0 -> (b_ip0'=ip0) & (n'=n+1);
[send0] l0>0 & n=1 -> (b_ip1'=ip0) & (n'=n+1);
[send0] l0>0 & n=2 -> (b_ip2'=ip0) & (n'=n+1);
[send0] l0>0 & n=3 -> (b_ip3'=ip0) & (n'=n+1);
[send0] l0>0 & n=4 -> (b_ip4'=ip0) & (n'=n+1);
[send0] l0>0 & n=5 -> (b_ip5'=ip0) & (n'=n+1);
[send0] l0>0 & n=6 -> (b_ip6'=ip0) & (n'=n+1);
[send0] l0>0 & n=7 -> (b_ip7'=ip0) & (n'=n+1);
[send0] l0>0 & n=8 -> (n'=n); // buffer full so lose message
[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
[] l0>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip'=b_ip0)
[] l>0 & b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0)
& (n'=n-1)
& (b_ip7'=0)
& (b_ip6'=b_ip7)
@ -165,16 +164,16 @@ module environment
& (b_ip0'=b_ip1); // lose message
// start sending message to host
[] l0>0 & b=0 & n0>0 -> (1-loss) : (b'=2) & (ip'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
[] l0>0 & b=0 & n1>0 -> (1-loss) : (b'=2) & (ip'=1) & (n1'=n1-1) + loss : (n1'=n1-1); // same ip
[] 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
[] l0>0 & b=1 & ip=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip'=0);
[] l0>0 & b=1 & ip=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip'=0);
[] l0>0 & b=1 & ip=2 -> (b'=0) & (z'=0) & (ip'=0);
[] 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
[rec0] l0>0 & b=2 -> (b'=0) & (z'=0) & (ip'=0);
[rec] l>0 & b=2 -> (b'=0) & (z'=0) & (ip_mess'=0);
endmodule
@ -182,17 +181,17 @@ endmodule
// CONCRETE HOST
module host0
y0 : [0..TIME_MAX_Y]; // second clock of the host
x0 : [0..TIME_MAX_X]; // clock of the host
x : [0..TIME_MAX_X]; // first clock of the host
y : [0..TIME_MAX_Y]; // second clock of the host
coll0 : [0..MAXCOLL]; // number of address collisions
probes0 : [0..K]; // counter (number of probes sent)
mess0 : [0..1]; // need to send a message or not
defend0 : [0..1]; // defend (if =1, try to defend IP address)
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)
ip0 : [1..2]; // ip address (1 - in use & 2 - fresh)
ip : [1..2]; // ip address (1 - in use & 2 - fresh)
l0 : [0..4] init 1; // location
l : [0..4] init 1; // location
// 0 : RECONFIGURE
// 1 : RANDOM
// 2 : WAITSP
@ -200,60 +199,60 @@ module host0
// 4 : USE
// RECONFIGURE
[reset0] l0=0 -> (l0'=1);
[reset] l=0 -> (l'=1);
// RANDOM (choose IP address)
[rec0] (l0=1) -> true; // get message (ignore since have no ip address)
[rec] (l=1) -> true; // get message (ignore since have no ip address)
// small number of collisions (choose straight away)
[] l0=1 & coll0<MAXCOLL -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2);
[] 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] l0=1 & coll0=MAXCOLL & y0<LONGWAIT -> (y0'=min(y0+1,TIME_MAX_Y));
[] l0=1 & coll0=MAXCOLL & y0=LONGWAIT -> 1/3*old : (l0'=2) & (ip0'=1) & (y0'=0)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=1)
+ 1/3*old : (l0'=2) & (ip0'=1) & (y0'=2)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=0)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=1)
+ 1/3*new : (l0'=2) & (ip0'=2) & (y0'=2);
[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] l0=2 & y0<2 -> (y0'=min(y0+1,2));
[time] l=2 & x<2 -> (x'=min(x+1,2));
// send probe
[send0] l0=2 & y0=2 & probes0<K -> (y0'=0) & (probes0'=probes0+1);
[send] l=2 & x=2 & probes<K -> (x'=0) & (probes'=probes+1);
// sent K probes and waited 2 seconds
[] l0=2 & y0=2 & probes0=K -> (l0'=3) & (probes0'=0) & (coll0'=0) & (y0'=0) & (x0'=2);
[] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
// get message and ip does not match: ignore
[rec0] l0=2 & ip!=ip0 -> (l0'=l0);
[rec] l=2 & ip_mess!=ip -> (l'=l);
// get a message with matching ip: reconfigure
[rec0] l0=2 & ip=ip0 -> (l0'=0) & (coll0'=min(coll0+1,MAXCOLL)) & (y0'=0) & (probes0'=0);
[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] l0=3 & mess0=0 & defend0=0 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X));
[time] l0=3 & mess0=0 & defend0=1 & x0<CONSEC -> (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND));
[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
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0>=DEFEND) -> (defend0'=1) & (mess0'=1) & (y0'=0);
[rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
// receive message and same ip: defer
[rec0] l0=3 & mess0=0 & ip=ip0 & (defend0=0 | y0<DEFEND) -> (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0);
[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
[rec0] l0=3 & mess0=0 & ip!=ip0 -> (l0'=l0);
[rec] l=3 & mess=0 & ip_mess!=ip -> (l'=l);
// send probe reply or message for defence
[send0] l0=3 & mess0=1 -> (mess0'=0);
[send] l=3 & mess=1 -> (mess'=0);
// send first gratuitous arp message
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0<1 -> (x0'=0) & (probes0'=probes0+1);
[send] l=3 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
// send second gratuitous arp message (move to use)
[send0] l0=3 & mess0=0 & x0=CONSEC & probes0=1 -> (l0'=4) & (x0'=0) & (y0'=0) & (probes0'=0);
[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)
[done] l0=4 -> true;
[] l=4 -> true;
endmodule
@ -265,6 +264,6 @@ module timer
t : [0..T+1];
[time] t<=T -> (t'=min(t+1,T+1));
[done] l0=4 -> (t'=T+1);
[done] l=4 -> (t'=T+1);
endmodule

4
prism-examples/zeroconf/zeroconf_time_bounded.pctl
View File

@ -1,4 +1,4 @@
// probability of using fresh ip address within time T
const int bound;
Pmin=?[ !(l0=4 & ip0=2) U t>bound ]
Pmax=?[ !(l0=4 & ip0=2) U t>bound ]
Pmin=?[ !(l=4 & ip=2) U t>bound ]
Pmax=?[ !(l=4 & ip=2) U t>bound ]
Write Preview
Loading…
Cancel
Save