pta
module robot
l : [0..5];
x : clock;
y : clock;
invariant
(l=0 => x<=4)
& (l=1 => x<=4)
& (l=2 => true)
& (l=3 => true)
& (l=4 => x<=4)
& (l=5 => x<=4)
endinvariant
[east] l=0 & x>=2 -> 0.6 : (l'=1) & (x'=0) + 0.4 : (l'=0) & (x'=0);
[south] l=0 & x>=2 & y<=8 -> 0.8 : (l'=3) & (x'=0) + 0.1 : (l'=1) & (x'=0) + 0.1 : (l'=4) & (x'=0);
[east] l=1 & x>=2 -> 1 : (l'=2) & (x'=0);
[south] l=1 & x>=2 & y<=8 -> 0.5 : (l'=4) & (x'=0) + 0.5 : (l'=2) & (x'=0);
[stuck] l=2 & x>=1 -> 1 : (l'=2) & (x'=0);
[stuck] l=3 & x>=1 -> 1 : (l'=3) & (x'=0);
[east] l=4 & x>=2 -> 1 : (l'=5) & (x'=0);
[west] l=4 & x>=2 -> 0.6 : (l'=3) & (x'=0) + 0.4 : (l'=4) & (x'=0);
[north] l=5 & x>=2 & y<=8 -> 0.9 : (l'=2) & (x'=0) + 0.1 : (l'=5) & (x'=0);
[west] l=5 & x>=2 -> 1 : (l'=4) & (x'=0);
endmodule
label "hazard" = l=1;
label "goal1" = l=5;
label "goal2" = l=2|l=3;
rewards "time"
true : 1;
endrewards