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