From 5b48be904ce78bc14463b17ba32a513365a4b79e Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Thu, 23 Jul 2009 12:34:27 +0000 Subject: [PATCH] fixes to zeroconf git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1317 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/zeroconf/zeroconf.nm | 133 +++++++++-------- prism-examples/zeroconf/zeroconf.pctl | 8 +- .../zeroconf/zeroconf_time_bounded.nm | 137 +++++++++--------- .../zeroconf/zeroconf_time_bounded.pctl | 4 +- 4 files changed, 140 insertions(+), 142 deletions(-) diff --git a/prism-examples/zeroconf/zeroconf.nm b/prism-examples/zeroconf/zeroconf.nm index 38bd391a..202de862 100644 --- a/prism-examples/zeroconf/zeroconf.nm +++ b/prism-examples/zeroconf/zeroconf.nm @@ -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 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 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 (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 (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 (y0'=0) & (probes0'=probes0+1); + [send] l=2 & x=2 & probes (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 (x0'=min(x0+1,TIME_MAX_X)); - [time] l0=3 & mess0=0 & defend0=1 & x0 (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND)); + [time] l=3 & mess=0 & defend=0 & x (x'=min(x+1,TIME_MAX_X)); + [time] l=3 & mess=0 & defend=1 & x (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 (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0); + [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y (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 diff --git a/prism-examples/zeroconf/zeroconf.pctl b/prism-examples/zeroconf/zeroconf.pctl index 3c15b2aa..ee1590e7 100644 --- a/prism-examples/zeroconf/zeroconf.pctl +++ b/prism-examples/zeroconf/zeroconf.pctl @@ -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 ] diff --git a/prism-examples/zeroconf/zeroconf_time_bounded.nm b/prism-examples/zeroconf/zeroconf_time_bounded.nm index 5557b9f2..df2ad776 100644 --- a/prism-examples/zeroconf/zeroconf_time_bounded.nm +++ b/prism-examples/zeroconf/zeroconf_time_bounded.nm @@ -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 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 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 (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 (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 (y0'=0) & (probes0'=probes0+1); + [send] l=2 & x=2 & probes (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 (x0'=min(x0+1,TIME_MAX_X)); - [time] l0=3 & mess0=0 & defend0=1 & x0 (x0'=min(x0+1,TIME_MAX_X)) & (y0'=min(y0+1,DEFEND)); + [time] l=3 & mess=0 & defend=0 & x (x'=min(x+1,TIME_MAX_X)); + [time] l=3 & mess=0 & defend=1 & x (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 (l0'=0) & (probes0'=0) & (defend0'=0) & (x0'=0) & (y0'=0); + [rec] l=3 & mess=0 & ip_mess=ip & (defend=0 | y (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 diff --git a/prism-examples/zeroconf/zeroconf_time_bounded.pctl b/prism-examples/zeroconf/zeroconf_time_bounded.pctl index 69b608ae..aa2030e9 100644 --- a/prism-examples/zeroconf/zeroconf_time_bounded.pctl +++ b/prism-examples/zeroconf/zeroconf_time_bounded.pctl @@ -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 ]