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

// 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