diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism
index 01d40c5..7a3119e 100644
--- a/velocity_safety_no_formulas.prism
+++ b/velocity_safety_no_formulas.prism
@@ -4,18 +4,25 @@ const int initY = 40;
 const int initX = 80;
 
 //const int maxY = 580;
-const int maxY = 300;
+//const int maxY = 430;
+const int maxY = 200;
 const int minX = 10;
 const int maxX = 152;
 const int maxVel = 8;
 
 
-formula Gate_1 = (((42<x & x<50) | (74<x  & x<82))   & 164<y & y<172);
+formula Gate_1 = (((42<x & x<50) | (74<x  & x<82))  & 164<y & y<172);
 formula Gate_2 = (((72<x & x<80) | (104<x & x<112)) & 256<y & y<264);
 formula Gate_3 = (((80<x & x<88) | (112<x & x<120)) & 349<y & y<357);
-formula Gate_4 = (((54<x & x<62) | (88<x  & x<96))   & 442<y & y<450);
+formula Gate_4 = (((54<x & x<62) | (88<x  & x<96))  & 442<y & y<450);
 formula Gate_5 = (((80<x & x<88) | (112<x & x<120)) & 530<y & y<538);
 
+formula S_Gate_1 = (((32<x & x<60) | (64<x  & x<92))  & 124<y & y<172);
+formula S_Gate_2 = (((62<x & x<90) | (94<x & x<132)) & 216<y & y<264);
+formula S_Gate_3 = (((70<x & x<98) | (102<x & x<130)) & 309<y & y<357);
+formula S_Gate_4 = (((44<x & x<72) | (78<x  & x<106))  & 402<y & y<450);
+formula S_Gate_5 = (((70<x & x<98) | (102<x & x<130)) & 490<y & y<538);
+
 
 formula Tree_1 = ((x>=124 & x<=142) & (y>=190 & y<=200));
 formula Tree_2 = ((x>=32 & x<=49)   & (y>=284 & y<=295));
@@ -24,26 +31,114 @@ formula Tree_4 = ((x>=12 & x<=30)   & (y>=408 & y<=418));
 formula Tree_5 = ((x>=129 & x<=146) & (y>=468 & y<=480));
 formula Tree_6 = ((x>=140 & x<=152) & (y>=496 & y<=510));
 
+formula S_Tree_1 = ((x>=114 & x<=152) & (y>=150 & y<=200));
+formula S_Tree_2 = ((x>=22 & x<=59)   & (y>=244 & y<=295));
+formula S_Tree_3 = ((x>=20 & x<=59)   & (y>=277 & y<=327));
+formula S_Tree_4 = ((x>=2 & x<=40)   & (y>=368 & y<=418));
+formula S_Tree_5 = ((x>=119 & x<=156) & (y>=438 & y<=480));
+formula S_Tree_6 = ((x>=130 & x<=162) & (y>=456 & y<=510));
+
 formula Hit_Tree = Tree_1 | Tree_2 | Tree_3 | Tree_4 | Tree_5 | Tree_6;
 formula Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5;
+formula S_Hit_Tree = S_Tree_1 | S_Tree_2 | S_Tree_3 | S_Tree_4 | S_Tree_5 | S_Tree_6;
+formula S_Hit_Gate = S_Gate_1 | S_Gate_2 | S_Gate_3 | S_Gate_4 | S_Gate_5;
 
 label "Hit_Tree" = Hit_Tree;
 label "Hit_Gate" = Hit_Gate;
+label "S_Hit_Tree" = S_Hit_Tree;
+label "S_Hit_Gate" = S_Hit_Gate;
 
 
 global move : [0..3];
 
-module skier
-  ski_position : [1..8] init 4;
-  done : bool init false;
 
 
-  [left]  !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
-  [right] !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
-  [noop]  !done & !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+module skier
+  ski_position : [1..8] init 4;
+  reward_given: bool init false;
+  //done: bool init false;
+
+
+  [left]  !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_1 & !Unsafe_1 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_1 |  Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_1 |  Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_1 |  Unsafe_1 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_2 & !Unsafe_2 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_2 |  Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_2 |  Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_2 |  Unsafe_2 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_3 & !Unsafe_3 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_3 |  Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_3 |  Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_3 |  Unsafe_3 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_4 & !Unsafe_4 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_4 |  Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_4 |  Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_4 |  Unsafe_4 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_5 & !Unsafe_5 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_5 |  Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_5 |  Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_5 |  Unsafe_5 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_6 & !Unsafe_6 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_6 |  Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_6 |  Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_6 |  Unsafe_6 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_7 & !Unsafe_7 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_7 |  Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_7 |  Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_7 |  Unsafe_7 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+  [left]  !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
+  [right] !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1);
+  [noop]  !reward_given & !Safe_8 & !Unsafe_8 & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
+  //[left]  !reward_given & (Safe_8 |  Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (reward_given'=true);
+  //[right] !reward_given & (Safe_8 |  Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (reward_given'=true);
+  //[noop]  !reward_given & (Safe_8 |  Unsafe_8 | Hit_Tree | Hit_Gate) & move=0 -> (move'=1) & (reward_given'=true);
+
+
+  //[left]  reward_given & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=true);
+  //[right] reward_given & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=true);
+  //[noop]  reward_given & move=0 -> (move'=1) & (done'=true);
+
+  [done] !reward_given & (Hit_Tree | Hit_Gate) & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_1 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_2 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_3 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_4 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_5 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_6 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_7 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Unsafe_8 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_1 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_2 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_3 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_4 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_5 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_6 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_7 & move=0 -> (reward_given'=true);
+  [done] !reward_given & Safe_8 & move=0 -> (reward_given'=true);
 
 
-  [done] move=0 & (Safe | Unsafe | Hit_Tree | Hit_Gate) -> (done'=true);
 endmodule
 
 module updateY
@@ -77,9 +172,18 @@ module updateX
   [update_x]  move=3 & standstill<8 & (ski_position=8)  -> 0.2: (x'=min(maxX,x+2)) & (move'=0) + 0.8: (x'=min(maxX,x+3)) & (move'=0);
 endmodule
 
+//rewards
+//  [left] !done & !reward_given & Hit_Tree : -100;
+//  [left] !done & !reward_given & Hit_Gate : -100;
+//  [left] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
+//  [right] !done & !reward_given & Hit_Tree : -100;
+//  [right] !done & !reward_given & Hit_Gate : -100;
+//  [right] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
+//  [noop] !done & !reward_given & Hit_Tree : -100;
+//  [noop] !done & !reward_given & Hit_Gate : -100;
+//  [noop] !done & !reward_given & (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8) : -100;
+//endrewards
+
 rewards
-  [done] !done & Hit_Tree : -100;
-  [done] !done & Hit_Gate : -100;
-  [done] !done & Unsafe : -100;
+  [done] !reward_given & (Hit_Gate | Hit_Tree | (Unsafe_1 | Unsafe_2 | Unsafe_3 | Unsafe_4 | Unsafe_5 | Unsafe_6 | Unsafe_7 | Unsafe_8)) : -100;
 endrewards
-