more dodge benchmarks

models/mdp/sketches/dodge/8-mod2-pull-30/sketch.templ

@@ -0,0 +1,102 @@
+mdp
+
+const int N=8;
+const int xMIN = 1;
+const int yMIN = 1;
+const int xMAX = N;
+const int yMAX = N;
+
+hole int x1_init in {1..8};
+hole int y1_init in {2..7};
+
+hole int a1_x0_y0 in {0,1,2,3,4};
+hole int a1_x0_y1 in {0,1,2,3,4};
+hole int a1_x1_y0 in {0,1,2,3,4};
+hole int a1_x1_y1 in {0,1,2,3,4};
+
+formula at1 = (x=x1 & y=y1);
+
+
+formula crash = at1;
+formula goal = (x=xMAX & y=yMAX);
+formula done = goal | crash;
+
+
+formula clk_next = mod(clk+1,2);
+module clk
+    clk : [-1..1] init -1;
+
+    [place] !done & clk=-1 -> (clk'=clk_next);
+
+    [left]  !done & clk=0 -> (clk'=clk_next);
+    [right] !done & clk=0 -> (clk'=clk_next);
+    [down]  !done & clk=0 -> (clk'=clk_next);
+    [up]    !done & clk=0 -> (clk'=clk_next);
+    [wait]  !done & clk=0 -> (clk'=clk_next);
+
+    [o]     !done & clk=1 -> (clk'=clk_next);
+endmodule
+
+
+const double slip = 0.2;
+
+formula xright  = min(x+1,xMAX);
+formula xleft   = max(x-1,xMIN);
+formula yup     = min(y+1,yMAX);
+formula ydown   = max(y-1,yMIN);
+
+module agent
+    x : [xMIN..xMAX] init xMIN;
+    y : [yMIN..yMAX] init yMIN;
+
+    [left]  true -> 1-slip : (x'=xleft)  + slip : (y'=ydown);
+    [right] true -> 1-slip : (x'=xright) + slip : (y'=yup);
+    [down]  true -> 1-slip : (y'=ydown)  + slip : (x'=xright);
+    [up]    true -> 1-slip : (y'=yup)    + slip : (x'=xleft);
+    //[wait]  true -> true;
+endmodule
+
+
+formula x1right  = min(x1+1,x1_init_MAX);
+formula x1left   = max(x1-1,x1_init_MIN);
+formula y1up     = min(y1+1,y1_init_MAX);
+formula y1down   = max(y1-1,y1_init_MIN);
+
+const double oslip = 1/2;
+module obstacle1
+    x1 : [xMIN..xMAX] init xMAX;
+    y1 : [yMIN..yMAX] init yMAX;
+
+    [place] true -> (x1'=x1_init) & (y1'=y1_init);
+
+    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_x0_y0=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_x0_y0=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_x0_y0=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_x0_y0=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_x0_y0=4 -> 1: true;
+
+    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_x0_y1=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_x0_y1=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_x0_y1=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_x0_y1=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_x0_y1=4 -> 1: true;
+
+    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_x1_y0=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_x1_y0=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_x1_y0=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_x1_y0=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_x1_y0=4 -> 1: true;
+
+    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_x1_y1=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_x1_y1=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_x1_y1=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_x1_y1=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_x1_y1=4 -> 1: true;
+
+endmodule
+
+const int battery_max = 30;
+module battery
+    battery : [0..battery_max] init battery_max;
+    [o] battery > 0 -> (battery'=battery-1);
+endmodule