//-------------------------------------------------------------
// model is an mdp
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 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
// size of buffers for other hosts
const int B0 = 4;  // buffer size for one abstract host
const int B1 = 4;  // buffer sizes for all abstract hosts

const int ip=1;
//-------------------------------------------------------------
// ENVIRONMENT - models: medium, output buffer of concrete host and all other hosts
module environment
	
	// buffer of concrete host
	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..4]; // 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'=(ip_mess=2)?2:0) // message being set
	               & (b_ip3'=(b_ip3=2)?2:0) 
	               & (b_ip2'=(b_ip2=2)?2:0) 
	               & (b_ip1'=(b_ip1=2)?2:0) 
	               & (b_ip0'=(b_ip0=2)?2: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 -> (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 -> (n'=n); // buffer full so lose message
	
	// start sending message from host
	[env] b=0 & n>0 -> (1-loss) : (b'=1) & (ip_mess'=b_ip0) 
	                                & (n'=n-1)
	                                & (b_ip3'=0) 
	                                & (b_ip2'=b_ip3) 
	                                & (b_ip1'=b_ip2) 
	                                & (b_ip0'=b_ip1) // send message
	                         + loss : (n'=n-1)
	                                & (b_ip3'=0) 
	                                & (b_ip2'=b_ip3) 
	                                & (b_ip1'=b_ip2) 
	                                & (b_ip0'=b_ip1); // lose message
	
	// start sending message to host
	[env] b=0 & n0>0 -> (1-loss) : (b'=2) & (ip_mess'=0) & (n0'=n0-1) + loss : (n0'=n0-1); // different ip
	[env] 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
	[env] b=1 & ip_mess=0 -> (b'=0) & (z'=0) & (n0'=min(n0+1,B0)) & (ip_mess'=0);
	[env] b=1 & ip_mess=1 -> (b'=0) & (z'=0) & (n1'=min(n1+1,B1)) & (ip_mess'=0);
	[env] 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
// 2 secs between send

module host_error1

	c : [0..2]; // time since first message
	s : [0..1];

	[time] s=0 -> true;
	// start counting
	[send1] s=0 -> (s'=1) & (c'=0);
	[send2] s=0 -> (s'=1) & (c'=0);
	[rec0] true -> (s'=0) & (c'=0);
	[rec1] true -> (s'=0) & (c'=0);
	// time passage so update relevant clocks
	[time] s=1 & c<1 -> (c'=c+1);
	[time] s=1 & c=1 -> (s'=0) & (c'=0);

endmodule

// reset must be preceeded by rec1 (with no time passage inbetween)
module host_error2

	s2 : [0..1];
	
	[time] true -> (s2'=0); 
	[rec1] true -> (s2'=1);
	[reset] s2=1 -> (s2'=0); 

endmodule

// records when a send1 or send2 action occurs
// and when rec0 and rec2 action occurs
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;
	[env] t=0 -> true;
	// note cannot do any action when t>0

endmodule