// IPv4: PTA model with digitial clocks // multi-objective model of the environment // gxn/dxp 28/09/09 mdp //------------------------------------------------------------- // VARIABLES const double loss = 0.1; // probability of message loss // 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 // 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 & (b_ip7'=0) & (b_ip6'=0) & (b_ip5'=0) & (b_ip4'=0) & (b_ip3'=0) & (b_ip2'=0) & (b_ip1'=0) & (b_ip0'=0); // time passage (only if no messages to send or sending a message) [time] b=0 & n=0 & n0=0 & n1=0 -> (b'=b); // cannot send a message [time] b>0 & z<1 -> (z'=min(z+1,TIME_MAX_Z)); // sending a message // get messages to be sent // message has ip address 1 [send1] n=0 -> (b_ip0'=1) & (n'=n+1); [send1] n=1 -> (b_ip1'=1) & (n'=n+1); [send1] n=2 -> (b_ip2'=1) & (n'=n+1); [send1] n=3 -> (b_ip3'=1) & (n'=n+1); [send1] n=4 -> (b_ip4'=1) & (n'=n+1); [send1] n=5 -> (b_ip5'=1) & (n'=n+1); [send1] n=6 -> (b_ip6'=1) & (n'=n+1); [send1] n=7 -> (b_ip7'=1) & (n'=n+1); [send1] n=8 -> (n'=n); // buffer full so lose message // message has ip address 2 [send2] n=0 -> (b_ip0'=2) & (n'=n+1); [send2] n=1 -> (b_ip1'=2) & (n'=n+1); [send2] n=2 -> (b_ip2'=2) & (n'=n+1); [send2] n=3 -> (b_ip3'=2) & (n'=n+1); [send2] n=4 -> (b_ip4'=2) & (n'=n+1); [send2] n=5 -> (b_ip5'=2) & (n'=n+1); [send2] n=6 -> (b_ip6'=2) & (n'=n+1); [send2] n=7 -> (b_ip7'=2) & (n'=n+1); [send2] n=8 -> (n'=n); // buffer full so lose message // start sending message from host [] 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 [] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip [] 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 [] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0); [] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0); [] b=1 & ip_mess=2 -> (b'=0) & (z'=0) & (ip_mess'=0); // finish sending message to host [rec0] b=2 & ip_mess=0 -> (b'=0) & (z'=0) & (ip_mess'=0); [rec1] b=2 & ip_mess=1 -> (b'=0) & (z'=0) & (ip_mess'=0); endmodule //------------------------------------------------------------- // assumption about the sender: only K send1's occur before one gets a rec1 // also the time between sends must be greater than 2 // since holds with certainty just removed transitions to error state and put in parallel const int K; module host_error count : [0..K]; t : [0..2]; host_done : [0..1]; // first send occurs [send1] host_done=0 & count=0 -> (count'=count+1); // send occurs: less than K has happended before a rec and 2 time units have passed since last [send1] host_done=0 & count<K & t=2 -> (count'=count+1) & (t'=0); // time passes [time] host_done=0 & count>0 -> (t'=min(t+1,2)); [time] host_done=0 & count=0 -> true; // rec occurs [rec1] host_done=0 -> (host_done'=1); // loop when error [send1] host_done=1 -> true; [time] host_done=1 -> true; [reset] host_done=1 -> true; [rec1] host_done=1 -> true; endmodule //------------------------------------------------------------- // error automaton for the environment assumption // do not get a reply when K probes are sent const int M; // time between sending and receiving a message module env_error4 env : [0..1]; // 0 active and 1 done k : [0..4]; // counts the number of messages sent c1 : [0..M+1]; // time since first message c2 : [0..M+1]; // time since second message c3 : [0..M+1]; // time since third message c4 : [0..M+1]; // time since fourth message error : [0..1]; // message with new ip address arrives so done [send2] error=0 & env=0 -> (env'=1); // message with old ip address arrives so count [send1] error=0 & env=0 -> (k'=min(k+1,K)); // time passgae so update relevant clocks [time] error=0 & env=0 & k=0 -> true; [time] error=0 & env=0 & k=1 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)); [time] error=0 & env=0 & k=2 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)); [time] error=0 & env=0 & k=3 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)); [time] error=0 & env=0 & k=4 & min(c1,c2,c3,c4)<M -> (c1'=min(c1+1,M+1)) & (c2'=min(c2+1,M+1)) & (c3'=min(c3+1,M+1)) & (c4'=min(c4+1,M+1)); // all clocks reached their bound so an error [time] error=0 & env=0 & min(c1,c2,c3,c4)=M -> (error'=1); // send a reply (then done) [rec1] error=0 & env=0 & k>0 & min(c1,c2,c3,c4)<=M -> (env'=1); // finished so any action can be performed [time] error=1 | env=1 -> true; [send1] error=1 | env=1 -> true; [send2] error=1 | env=1 -> true; [rec1] error=1 | env=1 -> true; endmodule