mdp

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);
	[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..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);
	[time] (r=0=>y+1<=0)&(r=1=>true)&(r=2=>y+1<=AD) -> 1.0 : (y'=min(y+1, 6));

endmodule