// simple tptg model from
// Verification and Control of Turn-Based Probabilistic Real-Time Games

tptg

player sender [send], [timeout] endplayer
player medium [arrive1], [arrive2] endplayer

module protocol

	l : [0..3] init 0;
	// 0 - send
	// 1 - medium
	// 2 - fail
	// 3 - done
	
	x : clock;
	y : clock;
	
	invariant
		(l=0 => (y<=24)) &
		(l=1 => (x<=4))
	endinvariant
		
	[send] l=0 & x>=1 & y<=22 -> (l'=1) & (x'=0);
	[timeout] l=0 & y=24 -> (l'=2);
	[arrive1] l=1 & x>=1 & x<=2 -> 0.9 : (l'=3) + 0.1 : (l'=0) & (x'=0);
	[arrive2] l=1 & x=4 -> (l'=3);
	
endmodule