mdp

// Dummy module to get PA semantics
module loops
	[] true -> true;
endmodule

// M1
const double p1 = 0.8;
module M1

	x : [0..3] init 0;

	[detect]   x=0 -> p1:(x'=1) + (1-p1):(x'=2);
	[warn]     x=1 -> (x'=2);
	[shutdown] x=2 -> (x'=3);
	[off]      x>2 -> true;

endmodule

// M2
const double p2 = 0.9;
module M2

	y : [0..3] init 0;

	[warn]     y=0 -> (y'=1);
	[shutdown] y=0 -> p2:(y'=2) + (1-p2):(y'=3);
	[shutdown] y=1 -> (y'=2);
	[off]      y=2 -> true;
	[fail]     y=3 -> true;
	
endmodule

// Error automaton for G (no fail)
label "err_G" = z=1;
module G_err

	z : [0..1] init 0;

	[fail] z=0 -> (z'=1);

	[fail] z=1 -> true;
	
endmodule