// prism model of pta version of zeroconf
// using digitial clocks

pta

const int probes_max = 4;

module sender

	s : [0..2]; //local state
	probes : [0..probes_max]; // probes sent
	ip : [0..2]; // ip address not chosen, fresh or in use
	x : clock; // local clock

	invariant
	(s=0 => x<=0) &
	(s=1 => x<=20) &
	(s=2 => true)
	endinvariant

	// selct probe	
	// [] s=0 -> 0.99969242125984251969 : (s'=1) & (ip'=0) + 0.00030757874015748031 : (s'=1) & (ip'=1);
	[] s=0 -> 0.5 : (s'=1) & (ip'=1) + 0.5 : (s'=1) & (ip'=2);
	// send probes
	[send_used]  s=1 & x=20 & ip=2 & probes<probes_max -> (probes'=probes+1) & (x'=0);	
	[send_fresh] s=1 & x=20 & ip=1 & probes<probes_max -> (probes'=probes+1) & (x'=0);
	//[] s=1 & x=20 & probes=probes_max -> (s'=2) & (x'=0);
	//[recv] s=1 -> (s'=0) & (x'=0) & (ip'=0) & (probes'=0);
	[] s=2 -> true;

endmodule