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