mdp

label "gains_information" = r=6;
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<=5)&(r=4=>y<=10)&(r=5=>true)&(r=6=>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..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);
	[] o=2&x>=AD -> (o'=4) & (x'=0);
	[done] o>=3 -> true;
	[time] (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..6];
	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=2 -> (r'=4) & (y'=0);
	[] r=3&y>=4 -> p*0.25 : (r'=6) & (y'=0) + (1-p)*0.25 : (r'=5) & (y'=0) + 0.75 : (r'=2) & (y'=0);
	[] r=4&y>=8 -> p : (r'=6) & (y'=0) + (1-p) : (r'=5) & (y'=0);
	[ack] r=5 -> (r'=1) & (y'=0);
	[time] (r=0=>y+1<=0)&(r=1=>true)&(r=2=>true)&(r=3=>y+1<=5)&(r=4=>y+1<=10)&(r=5=>true)&(r=6=>true) -> 1.0 : (y'=min(y+1, 11));

endmodule