smg

// originator
player p1
  originator, [message], [time1]
endplayer

// environment
player p2
  recipient, [req], [ack], [time2], [end]
endplayer


label "gains_information" = r=5;
label "invariants" = (o=0=>true)&(o=1=>x<=MD)&(o=2=>x<=AD)&(o=3=>true)&(o=4=>true)&(r=0=>y<=0)&(r=1=>true)&(r=2=>true)&(r=3=>y<=10)&(r=4=>true)&(r=5=>true);

const double p;
const int ad = 1;
const int AD = 5;
const int md = 2;
const int MD = 9;

module originator

	o : [0..4];
	x : [0..6];

	[req] o=0 -> (o'=1) & (x'=0);
	[message] o=1&x>=md -> (o'=2) & (x'=0);
	[ack] o=2&x<=AD -> 1-p : (o'=1) & (x'=0) + p : (o'=3) & (x'=0);
	[end] o=2&x>=AD -> (o'=4) & (x'=0); // cannot have this as no longer turn based
	[time1] r=1 & o<=2 & (o=0=>true)&(o=1=>x+1<=MD)&(o=2=>x+1<=AD)&(o=3=>true)&(o=4=>true) -> 1.0 : (x'=min(x+1,10));
	[time2] !(r=1 & o<=2) & (o=0=>true)&(o=1=>x+1<=MD)&(o=2=>x+1<=AD)&(o=3=>true)&(o=4=>true) -> 1.0 : (x'=min(x+1,10));

endmodule

module recipient

	r : [0..9];
	y : [0..11];

	[req] r=0&y=0 -> (r'=1);
	[message] r=1 -> (r'=2) & (y'=0);
	[ack] r=2 -> (r'=1);
	[] r=2 -> (r'=3) & (y'=0);
	[] r=3&y>=8 -> p : (r'=5) & (y'=0) + (1-p) : (r'=4) & (y'=0);
	[ack] r=4 -> (r'=1) & (y'=0);
	[time1] r=1 & o<=2 & (r=0=>y+1<=0)&(r=1=>true)&(r=2=>true)&(r=3=>y+1<=10)&(r=4=>true)&(r=5=>true) -> 1.0 : (y'=min(y+1, 11));
	[time2] !(r=1 & o<=2) & (r=0=>y+1<=0)&(r=1=>true)&(r=2=>true)&(r=3=>y+1<=10)&(r=4=>true)&(r=5=>true) -> 1.0 : (y'=min(y+1, 11));

endmodule

const int K; // deadline

module timer
	
	t : [0..K+1];
	
	[time1] true -> (t'=min(t+1,K+1));
	[time2] true -> (t'=min(t+1,K+1));
	
endmodule