add obstacles with uniform belief

models/pomdp/sketches/obstacles-uniform/sketch.props

@@ -0,0 +1 @@
+R{"penalty"}min=? [ F goal ];

models/pomdp/sketches/obstacles-uniform/sketch.templ

@@ -0,0 +1,107 @@
+pomdp
+
+// grid dimensions
+const int N = 10;
+const int xMIN = 0;
+const int yMIN = 0;
+const int xMAX = N-1;
+const int yMAX = N-1;
+
+formula goal = (x=xMAX & y=yMAX);
+
+observable "clk" = clk;
+observable "goal" = goal;
+observable "x_small" = x<(xMAX/2);
+observable "y_small" = y<(yMAX/2);
+
+module hole_clk
+    hole_clk : [0..4] init 0;
+    [hole_init] hole_clk<4 -> (hole_clk'=hole_clk+1);
+    [place]     hole_clk=4 -> true;
+endmodule
+
+module hole_init
+    o1x : [3..5];
+    o1y : [3..5];
+    o2x : [6..8];
+    o2y : [6..8];
+
+    [hole_init] hole_clk=0 -> 1/3:(o1x'=3)+1/3:(o1x'=4)+1/3:(o1x'=5);
+    [hole_init] hole_clk=1 -> 1/3:(o1y'=3)+1/3:(o1y'=4)+1/3:(o1y'=5);
+    [hole_init] hole_clk=2 -> 1/3:(o2x'=6)+1/3:(o2x'=7)+1/3:(o2x'=8);
+    [hole_init] hole_clk=3 -> 1/3:(o2y'=6)+1/3:(o2y'=7)+1/3:(o2y'=8);
+endmodule
+
+formula near1 = 3<=x & x<=5 & 3<=y & y<=5;
+formula near2 = 6<=x & x<=8 & 6<=y & y<=8;
+//formula near3 = 1<=x & x<=3 & 3<=y & y<=4;
+//formula near4 = 3<=x & x<=4 & 1<=y & y<=3;
+
+formula at1 = (x = o1x & y = o1y);
+formula at2 = (x = o2x & y = o2y);
+//formula at3 = (x = o3x & y = o3y);
+//formula at4 = (x = o4x & y = o4y);
+
+const NUM_OBS = 2;
+
+formula clk_next = mod(clk+1,NUM_OBS+1);
+module clk
+    clk : [-1..NUM_OBS] init -1;
+
+    [place] clk=-1 -> (clk'=clk_next);
+
+    [up]    !goal & clk=0 -> (clk'=clk_next);
+    [down]  !goal & clk=0 -> (clk'=clk_next);
+    [left]  !goal & clk=0 -> (clk'=clk_next);
+    [right] !goal & clk=0 -> (clk'=clk_next);
+
+    [detect1] !goal & clk=1 -> (clk'=clk_next);
+    [detect2] !goal & clk=2 -> (clk'=clk_next);
+    [detect3] !goal & clk=3 -> (clk'=clk_next);
+    [detect4] !goal & clk=4 -> (clk'=clk_next);
+endmodule
+
+
+// probability of slipping 2 cells ahead
+const double slip = 0.1;
+
+// moving around the grid
+module agent
+    x : [xMIN..xMAX];
+    y : [yMIN..yMAX];
+
+    [place] true ->  1/4: (x'=o1x-1) & (y'=o1y) + 1/4: (x'=1) & (y'=1) + 1/4: (x'=2) & (y'=1) + 1/4: (x'=1) & (y'=3);
+
+    [up]    true -> (1-slip): (y'=max(y-1,yMIN)) + slip: (y'=max(y-2,yMIN));
+    [down]  true -> (1-slip): (y'=min(y+1,yMAX)) + slip: (y'=min(y+2,yMAX));
+    [left]  true -> (1-slip): (x'=max(x-1,xMIN)) + slip: (x'=max(x-2,xMIN));
+    [right] true -> (1-slip): (x'=min(x+1,xMAX)) + slip: (x'=min(x+2,xMAX));
+endmodule
+
+// crash detection
+module crash1
+    crash1 : bool init false;
+    [detect1]  near1 -> (crash1'=at1);
+    [detect1] !near1 -> true;
+
+    [up]    true -> (crash1'=false);
+    [down]  true -> (crash1'=false);
+    [left]  true -> (crash1'=false);
+    [right] true -> (crash1'=false);
+endmodule
+
+module crash2=crash1[crash1=crash2,detect1=detect2,near1=near2,at1=at2] endmodule
+//module crash3=crash1[crash1=crash3,detect1=detect3,near1=near3,at1=at3] endmodule
+//module crash4=crash1[crash1=crash4,detect1=detect4,near1=near4,at1=at4] endmodule
+
+formula step_penalty = 1;
+formula crash_penalty = 100;
+formula num_crashes = (crash1?1:0)+(crash2?1:0);
+formula penalty = step_penalty + num_crashes*crash_penalty;
+
+rewards "penalty"
+    [up]    true : penalty;
+    [down]  true : penalty;
+    [left]  true : penalty;
+    [right] true : penalty;
+endrewards