pomdp
observables
o
endobservables
module grid
x : [0..2];
y : [0..2];
o : [0..2];
[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+ 1/8 : (o'=1) & (x'=1) & (y'=2)
+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+ 1/8 : (o'=1) & (x'=2) & (y'=2);
[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2));
[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2);
[west] o=1 -> (x'=max(x-1,0));
[north] o=1 -> (x'=min(y+1,2));
[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0));
[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2);
[done] o=2 -> true;
endmodule
rewards
[east] true : 1;
[west] true : 1;
[north] true : 1;
[south] true : 1;
endrewards