// IPv4: PTA model with digitial clocks
// multi-objective model of the host for initial assumption
// gxn/dxp 28/09/09

mdp

//-------------------------------------------------------------
// VARIABLES
const int N=20; // number of abstract hosts
const int K; // number of probes to send

// PROBABILITIES
const double old = N/65024; // probability pick an ip address being used
//const double old = 0.5; // 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


//-------------------------------------------------------------
// 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) -> 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
	[send1] l=2 & ip=1 & x=2  & probes<K -> (x'=0) & (probes'=probes+1);
	[send2] l=2 & ip=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
	[rec2] l=2 & ip=2 -> (l'=l);
	// get a message with matching ip: reconfigure
	[rec1] l=2 & ip=1 -> (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
	[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y>=DEFEND) -> (defend'=1) & (mess'=1) & (y'=0);
	// receive message and same ip: defer
	[rec1] l=3 & mess=0 & ip=1 & (defend=0 | y<DEFEND) -> (l'=0) & (probes'=0) & (defend'=0) & (x'=0) & (y'=0);
	// receive message and different ip
	[rec2] l=3 & mess=0 & ip=2 -> (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 -> true;
	
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
module host_error

	count : [0..K];
	t : [0..2];
	host_err : [0..1];
	host_done : [0..1];
	
	// first send occurs 
	[send1] host_done=0 & host_err=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 & host_err=0 & count<K & t=2 -> (count'=count+1) & (t'=0); 
	// more than k sends occur in a row - error 
	[send1] host_done=0 & host_err=0 & count=K -> (host_err'=1);
	// time passes
	[time] host_done=0 & host_err=0 & count>0 -> (t'=min(t+1,2));
	[time] host_done=0 & host_err=0 & count=0 -> true;
	// rec occurs
	[rec1] host_done=0  -> (host_done'=1);

	// loop when error
	[send1] host_done=1 | host_err=1-> true;
	[time] host_done=1 | host_err=1-> true;
	[reset] host_done=1 | host_err=1-> true;
	[rec1] host_done=1 | host_err=1-> true;

endmodule