mdp

module one
	x : [0 .. 2] init 0;

	[a] x = 0 -> (x'=1);
	[] x = 1 -> true;
endmodule

module two
	y : [0 .. 2] init 0;

	[b] y=0 -> (y'=1);
	[] y=1 -> true;
endmodule

module three
	z : [0 .. 2] init 0;

	[c] z=0 -> (z'=1);
	[] z=1 -> true;
endmodule

system
	((one || two) {a <- b} |[a]| (three {a <- c})) / {a, b, c}
endsystem