mdp
module loops
[] true -> true;
endmodule
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
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
label "err_G" = z=1;
module G_err
z : [0..1] init 0;
[fail] z=0 -> (z'=1);
[fail] z=1 -> true;
endmodule