// model is an mdp
mdp

// rewards expected time until configured
rewards

	[time] l<4 : 1;
	
endrewards

//-------------------------------------------------------------
// 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 = 1/4; // 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 TIME_MAX_X = 60; // max value of clock x
const int TIME_MAX_Z = 1;  // max value of clock z

// OTHER CONSTANTS
const int MAXCOLL = 10;  // maximum number of collisions before long wait

formula ip_mess = ip;

//-------------------------------------------------------------
// CONCRETE HOST
module host0
	
	x : [0..TIME_MAX_X]; // first 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
	
	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)
	[rec0] (l=1) -> true; // get message (ignore since have no ip address)
	[rec1] (l=1) -> true; // get message (ignore since have no ip address)
	// small number of collisions (choose straight away)
	[host] l=1 -> 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)
	// if i delete this line everything works
	[time] l=1 & coll=MAXCOLL & x<LONGWAIT -> (x'=min(x+1,TIME_MAX_X));
	[host] 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
	[host] l=2 & x=2 & probes=K -> (l'=3) & (probes'=0) & (coll'=0) & (x'=0);
	// get message and ip does not match: ignore
	[rec0] l=2 & ip!=0 -> (l'=l);
	[rec1] l=2 & ip!=1 -> (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 & x<CONSEC -> (x'=min(x+1,TIME_MAX_X)); 
	
	// receive message and same ip: suppose always defer
	[rec1] l=3 & mess=0 & ip=1 -> (l'=0) & (probes'=0) & (x'=0);
	// receive message and different ip
	[rec0] l=3 & mess=0 & ip!=0 -> (l'=l);
	[rec1] l=3 & mess=0 & ip!=1 -> (l'=l);
	
		
	// send probe reply or message for defence
	[send1] l=3 & ip=1 & mess=1 -> (mess'=0);
	[send2] l=3 & ip=2 & mess=1 -> (mess'=0);
	// send first gratuitous arp message
	[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
	[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes<1 -> (x'=0) & (probes'=probes+1);
	// send second gratuitous arp message (move to use)
	[send1] l=3 & ip=1 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (probes'=0);
	[send2] l=3 & ip=2 & mess=0 & x=CONSEC & probes=1 -> (l'=4) & (x'=0) & (probes'=0);
	
	// USE (only interested in reaching this state so do not need to add anything here)
	[host] l=4 -> true;
	
endmodule

//-------------------------------------------------------------

// records when a time action or send1 action occurs (needed in properties)
module timer

	t : [0..2];
	
	[send1] t=0 -> (t'=1);
	[send2] t=0 -> (t'=1);
	[rec0] t=0 -> (t'=2);
	[rec1] t=0 -> (t'=2);
	[] t>0 -> (t'=0);
	
	// can do all actions when t=0
	[time] t=0 -> true;
	[reset] t=0 -> true;
	[host] t=0 -> true;
	// note cannot do anything when t=1

endmodule