diff --git a/models/mdp/sketches/dodge/10-1/sketch.templ b/models/mdp/sketches/dodge/10-1/sketch.templ
deleted file mode 100755
index f806a8877..000000000
--- a/models/mdp/sketches/dodge/10-1/sketch.templ
+++ /dev/null
@@ -1,114 +0,0 @@
-mdp
-
-const int N=10;
-const int xMIN = 1;
-const int yMIN = 1;
-const int xMAX = N;
-const int yMAX = N;
-
-hole int x1_init in {1..10};
-hole int y1_init in {2..9};
-
-hole int a1_xeve_yeve in {0,1,2};
-hole int a1_xeve_yodd in {0,1,2};
-hole int a1_xodd_yodd in {0,1,2};
-hole int a1_xodd_yeve in {0,1,2};
-
-formula at1 = (x=x1 & y=y1);
-
-
-//hole int x2_init in {1..6};
-//hole int y2_init in {4..5};
-
-// hole int a2_xeve_yeve in {0,1,2};
-// hole int a2_xeve_yodd in {0,1,2};
-// hole int a2_xodd_yodd in {0,1,2};
-// hole int a2_xodd_yeve in {0,1,2};
-
-//formula at2 = (x=x2 & y=y2);
-
-
-formula crash = at1;
-//formula crash = at1 | at2;
-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 : true;
-    [right] true -> 1-slip : (x'=xright) + slip : true;
-    [down]  true -> 1-slip : (y'=ydown)  + slip : true;
-    [up]    true -> 1-slip : (y'=yup)    + slip : true;
-    //[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);
-
-// formula x2right  = min(x2+1,x2_init_MAX);
-// formula x2left   = max(x2-1,x2_init_MIN);
-// formula y2up     = min(y2+1,y2_init_MAX);
-// formula y2down   = max(y2-1,y2_init_MIN);
-
-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_xeve_yeve=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=4 -> 1: true;
-
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=4 -> 1: true;
-
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=4 -> 1: true;
-
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=4 -> 1: true;
-
-endmodule
-
-// module obstacle2=obstacle1[x1=x2,y1=y2,x1_init=x2_init,y1_init=y2_init,x1right=x2right,x1left=x2left,y1up=y2up,y1down=y2down,a1_xeve_yeve=a2_xeve_yeve,a1_xeve_yodd=a2_xeve_yodd,a1_xodd_yodd=a2_xodd_yodd,a1_xodd_yeve=a2_xodd_yeve] endmodule
\ No newline at end of file
diff --git a/models/mdp/sketches/dodge/6-1/sketch.templ b/models/mdp/sketches/dodge/6-1/sketch.templ
deleted file mode 100755
index 95a87539b..000000000
--- a/models/mdp/sketches/dodge/6-1/sketch.templ
+++ /dev/null
@@ -1,114 +0,0 @@
-mdp
-
-const int N=6;
-const int xMIN = 1;
-const int yMIN = 1;
-const int xMAX = N;
-const int yMAX = N;
-
-hole int x1_init in {1..6};
-hole int y1_init in {2..5};
-
-hole int a1_xeve_yeve in {0,1,2};
-hole int a1_xeve_yodd in {0,1,2};
-hole int a1_xodd_yodd in {0,1,2};
-hole int a1_xodd_yeve in {0,1,2};
-
-formula at1 = (x=x1 & y=y1);
-
-
-//hole int x2_init in {1..6};
-//hole int y2_init in {4..5};
-
-// hole int a2_xeve_yeve in {0,1,2};
-// hole int a2_xeve_yodd in {0,1,2};
-// hole int a2_xodd_yodd in {0,1,2};
-// hole int a2_xodd_yeve in {0,1,2};
-
-//formula at2 = (x=x2 & y=y2);
-
-
-formula crash = at1;
-//formula crash = at1 | at2;
-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 : true;
-    [right] true -> 1-slip : (x'=xright) + slip : true;
-    [down]  true -> 1-slip : (y'=ydown)  + slip : true;
-    [up]    true -> 1-slip : (y'=yup)    + slip : true;
-    //[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);
-
-// formula x2right  = min(x2+1,x2_init_MAX);
-// formula x2left   = max(x2-1,x2_init_MIN);
-// formula y2up     = min(y2+1,y2_init_MAX);
-// formula y2down   = max(y2-1,y2_init_MIN);
-
-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_xeve_yeve=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=0 & a1_xeve_yeve=4 -> 1: true;
-
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=0 & mod(y1,2)=1 & a1_xeve_yodd=4 -> 1: true;
-
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=0 & a1_xodd_yeve=4 -> 1: true;
-
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=0 -> 1/2 : (x1'=x1right) + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=1 -> 1/2 : (x1'=x1left)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=2 -> 1/2 : (y1'=y1up)    + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=3 -> 1/2 : (y1'=y1down)  + 1/2 : true;
-    [o]  mod(x1,2)=1 & mod(y1,2)=1 & a1_xodd_yodd=4 -> 1: true;
-
-endmodule
-
-// module obstacle2=obstacle1[x1=x2,y1=y2,x1_init=x2_init,y1_init=y2_init,x1right=x2right,x1left=x2left,y1up=y2up,y1down=y2down,a1_xeve_yeve=a2_xeve_yeve,a1_xeve_yodd=a2_xeve_yodd,a1_xodd_yodd=a2_xodd_yodd,a1_xodd_yeve=a2_xodd_yeve] endmodule
\ No newline at end of file
diff --git a/models/mdp/sketches/dodge/10-1/sketch.props b/models/mdp/sketches/dodge/8-mod2-pull-30/sketch.props
similarity index 100%
rename from models/mdp/sketches/dodge/10-1/sketch.props
rename to models/mdp/sketches/dodge/8-mod2-pull-30/sketch.props
diff --git a/models/mdp/sketches/dodge/8-mod2-pull-30/sketch.templ b/models/mdp/sketches/dodge/8-mod2-pull-30/sketch.templ
new file mode 100755
index 000000000..b73ffa420
--- /dev/null
+++ b/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
diff --git a/models/mdp/sketches/dodge/6-1/sketch.props b/models/mdp/sketches/dodge/8-mod2-stagger-30/sketch.props
similarity index 100%
rename from models/mdp/sketches/dodge/6-1/sketch.props
rename to models/mdp/sketches/dodge/8-mod2-stagger-30/sketch.props
diff --git a/models/mdp/sketches/dodge/8-mod2-stagger-30/sketch.templ b/models/mdp/sketches/dodge/8-mod2-stagger-30/sketch.templ
new file mode 100755
index 000000000..711ff5a23
--- /dev/null
+++ b/models/mdp/sketches/dodge/8-mod2-stagger-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 : true;
+    [right] true -> 1-slip : (x'=xright) + slip : true;
+    [down]  true -> 1-slip : (y'=ydown)  + slip : true;
+    [up]    true -> 1-slip : (y'=yup)    + slip : true;
+    //[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
diff --git a/models/mdp/sketches/dodge/8-mod2-stagger/sketch.props b/models/mdp/sketches/dodge/8-mod2-stagger/sketch.props
new file mode 100755
index 000000000..6387655d3
--- /dev/null
+++ b/models/mdp/sketches/dodge/8-mod2-stagger/sketch.props
@@ -0,0 +1 @@
+P>0.9 [F goal]
\ No newline at end of file
diff --git a/models/mdp/sketches/dodge/8-mod2-stagger/sketch.templ b/models/mdp/sketches/dodge/8-mod2-stagger/sketch.templ
new file mode 100755
index 000000000..d1f192cce
--- /dev/null
+++ b/models/mdp/sketches/dodge/8-mod2-stagger/sketch.templ
@@ -0,0 +1,96 @@
+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 : true;
+    [right] true -> 1-slip : (x'=xright) + slip : true;
+    [down]  true -> 1-slip : (y'=ydown)  + slip : true;
+    [up]    true -> 1-slip : (y'=yup)    + slip : true;
+    //[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
diff --git a/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.props b/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.props
new file mode 100755
index 000000000..6387655d3
--- /dev/null
+++ b/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.props
@@ -0,0 +1 @@
+P>0.9 [F goal]
\ No newline at end of file
diff --git a/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.templ b/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.templ
new file mode 100755
index 000000000..321dc0a8c
--- /dev/null
+++ b/models/mdp/sketches/dodge/8-mod3-pull-30/sketch.templ
@@ -0,0 +1,133 @@
+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_x0_y2 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};
+hole int a1_x1_y2 in {0,1,2,3,4};
+hole int a1_x2_y0 in {0,1,2,3,4};
+hole int a1_x2_y1 in {0,1,2,3,4};
+hole int a1_x2_y2 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,3)=0 & mod(y1,3)=0 & a1_x0_y0=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=0 & a1_x0_y0=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=0 & a1_x0_y0=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=0 & a1_x0_y0=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=0 & a1_x0_y0=4 -> 1: true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=1 & a1_x0_y1=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=1 & a1_x0_y1=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=1 & a1_x0_y1=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=1 & a1_x0_y1=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=1 & a1_x0_y1=4 -> 1: true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=2 & a1_x0_y2=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=2 & a1_x0_y2=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=2 & a1_x0_y2=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=2 & a1_x0_y2=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=0 & mod(y1,3)=2 & a1_x0_y2=4 -> 1: true;
+
+    
+    [o]  mod(x1,3)=1 & mod(y1,3)=0 & a1_x1_y0=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=0 & a1_x1_y0=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=0 & a1_x1_y0=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=0 & a1_x1_y0=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=0 & a1_x1_y0=4 -> 1: true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=1 & a1_x1_y1=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=1 & a1_x1_y1=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=1 & a1_x1_y1=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=1 & a1_x1_y1=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=1 & a1_x1_y1=4 -> 1: true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=2 & a1_x1_y2=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=2 & a1_x1_y2=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=2 & a1_x1_y2=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=2 & a1_x1_y2=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=1 & mod(y1,3)=2 & a1_x1_y2=4 -> 1: true;
+
+
+    [o]  mod(x1,3)=2 & mod(y1,3)=0 & a1_x2_y0=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=0 & a1_x2_y0=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=0 & a1_x2_y0=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=0 & a1_x2_y0=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=0 & a1_x2_y0=4 -> 1: true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=1 & a1_x2_y1=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=1 & a1_x2_y1=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=1 & a1_x2_y1=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=1 & a1_x2_y1=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=1 & a1_x2_y1=4 -> 1: true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=2 & a1_x2_y2=0 -> 1-oslip : (x1'=x1right) + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=2 & a1_x2_y2=1 -> 1-oslip : (x1'=x1left)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=2 & a1_x2_y2=2 -> 1-oslip : (y1'=y1up)    + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=2 & a1_x2_y2=3 -> 1-oslip : (y1'=y1down)  + oslip : true;
+    [o]  mod(x1,3)=2 & mod(y1,3)=2 & a1_x2_y2=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
diff --git a/models/mdp/sketches/rocks/8-1/sketch.props b/models/mdp/sketches/rocks/8-1/sketch.props
deleted file mode 100755
index 456b7a259..000000000
--- a/models/mdp/sketches/rocks/8-1/sketch.props
+++ /dev/null
@@ -1 +0,0 @@
-P>=1 [F goal]
diff --git a/models/mdp/sketches/rocks/8-1/sketch.templ b/models/mdp/sketches/rocks/8-1/sketch.templ
deleted file mode 100755
index d89ccab13..000000000
--- a/models/mdp/sketches/rocks/8-1/sketch.templ
+++ /dev/null
@@ -1,56 +0,0 @@
-mdp
-
-const int N = 8;
-const int xMIN = 1;
-const int yMIN = 1;
-const int xMAX = N;
-const int yMAX = N;
-
-hole int o1x in {1..8};
-hole int o1y in {1..8};
-
-formula at1 = (x = o1x & y = o1y);
-
-formula near1 = o1x_MIN<=x & x<=o1x_MAX & o1y_MIN<=y & y<=o1y_MAX;
-
-const NUM_OBS = 1;
-formula crash = false;
-formula goal = visit1;
-formula done = goal | crash;
-
-
-formula clk_next = mod(clk+1,NUM_OBS+1);
-module clk
-    clk : [0..NUM_OBS] init 0;
-
-    [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);
-    
-    [detect1] !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);
-endmodule
-
-module visit1
-    visit1 : bool init false;
-    [detect1] !near1 |  visit1 -> true;
-    [detect1]  near1 & !visit1 -> (visit1'=at1);
-endmodule