smg

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

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

label "terminated_successfully" = o=3;
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=>y<=AD);

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..10];

	[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);
	[time1] r=1 & o<=2 & (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=2=>x+1<=AD)&(o=3=>true)&(o=4=>true) -> 1.0 : (x'=min(x+1,10));

endmodule

module recipient

	r : [0..3];
	y : [0..6];

	[req] r=0&y=0 -> (r'=1);
	[message] r=1 -> (r'=2) & (y'=0);
	[ack] r=2&y>=ad -> (r'=1) & (y'=0);
	[time1] r=1 & o<=2 & (r=1=>true)&(r=0=>y+1<=0)&(r=2=>y+1<=AD) -> 1.0 : (y'=min(y+1, 6));
	[time2] !(r=1 & o<=2) & (r=1=>true)&(r=0=>y+1<=0)&(r=2=>y+1<=AD) -> 1.0 : (y'=min(y+1, 6));

endmodule

rewards "time"
	[time1] true : 1;
	[time2] true : 1;	
endrewards