mdp

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..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);
	[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..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);
	[time] (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