mdp

// Dummy module to get PA semantics
module loops
	[] true -> 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 A1 (never shutdown before warn)
label "err_A" = a=2;
module A_err

	a : [0..3] init 0;

	[warn]     a=0 -> (a'=1);
	[shutdown] a=0 -> (a'=2);

	[warn]     a>=1 -> true;
	[shutdown] a>=1 -> 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