mdp
const double p_fail = 0.1;
const int jmax = 2;
module M_m
j : [0..jmax];
on : bool init true;
[fast] on & j<jmax -> p_fail:(j'=j) + (1-p_fail):(j'=j+1);
[slow] on & j<jmax -> (j'=j+1);
[off] on & j<jmax -> (on'=false);
[on] !on & j<jmax -> (on'=true);
[done] j=jmax -> true;
endmodule
label "A1_K" = a1=1;
module A1
a1 : [0..1] init 0;
[off] true -> (a1'=1);
endmodule
rewards "fast"
[fast] true : 1;
endrewards
rewards "slow"
[slow] true : 1;
endrewards
rewards "time"
[fast] true : 1;
[slow] true : 3;
endrewards