popta

observables
	x, y, o
endobservables

module M

	l : [0..5] init 0;
	o : [0..4] init 0; // 0, 1&2, 3, 4, 5
	x : clock;
	y : clock;

	invariant
		(l=0 => x<=1) &
		(l=1 => true) &
		(l=2 => true) &
		(l=3 => true) &
		(l=4 => true) &
		(l=5 => true)
	endinvariant

	[a0] l=0 & x>=1 -> 1/2 : (l'=1)&(o'=1) + 1/2 : (l'=2)&(o'=1);
	[a] l=1 -> (l'=3)&(o'=2);
	[a] l=2 -> (l'=4)&(o'=3)&(x'=0);
	[b] l=3 & y=1 -> (l'=5)&(o'=4);
	[b] l=4 & y=2 & x=0 -> (l'=5)&(o'=4);

endmodule

label "goal" = o=4;