From 746795cd40f4b78b3a48c3bdb44c87ae78362e16 Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Mon, 6 May 2024 08:36:47 +0200
Subject: [PATCH] added vanilla mdp file

---
 velocity_safety_no_formulas.prism | 84 +++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 velocity_safety_no_formulas.prism

diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism
new file mode 100644
index 0000000..e49d30a
--- /dev/null
+++ b/velocity_safety_no_formulas.prism
@@ -0,0 +1,84 @@
+mdp
+
+const int initY = 40;
+const int initX = 80;
+
+const int maxY = 580;
+const int minX = 10;
+const int maxX = 144;
+
+
+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_5 = (((80<x & x<88) | (112<x & x<120)) & 530<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));
+formula Tree_3 = ((x>=30 & x<=49)   & (y>=317 & y<=327));
+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 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;
+
+
+global move : [0..3];
+
+module skier
+  ski_position : [1..8] ;
+  done : bool ;
+
+
+  [left]  !Safe & !Unsafe & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate));
+  [right] !Safe & !Unsafe & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate));
+  [noop]  !Safe & !Unsafe & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate));
+
+
+  [done] Safe | Unsafe | done -> true;
+endmodule
+
+module updateY
+  y : [initY..maxY] ;
+
+  velocity: [0..16];
+  standstill : [0..8] ;
+  [update_y] move=1 & standstill>=5 -> (y'=y) & (move'=2);
+  [update_y] move=1 & standstill<5  -> (y'=min(maxY,y+velocity)) & (move'=2);
+
+  [update_y] move=2 & (ski_position=1 | ski_position = 8) & standstill>=5 -> (standstill'=min(8,standstill+1)) & (move'=3);
+  [update_y] move=2 & (ski_position=1 | ski_position = 8) & standstill<5  -> (velocity'=max(0,velocity-4)) &(move'=3);
+  [update_y] move=2 & (ski_position=2 | ski_position = 7) -> (velocity'=max(0 ,velocity-2)) & (standstill'=0) & (move'=3);
+  [update_y] move=2 & (ski_position=3 | ski_position = 6) -> (velocity'=min(8,velocity+2)) & (standstill'=0) & (move'=3);
+  [update_y] move=2 & (ski_position=4 | ski_position = 5) -> (velocity'=min(8,velocity+4)) & (standstill'=0) & (move'=3);
+endmodule
+
+module updateX
+  x : [minX..maxX] ;
+
+  [update_x]  move=3 & standstill>=8                                       -> (move'=0);
+  [update_x]  move=3 & standstill<8 & (ski_position=4 | ski_position=5)    -> (move'=0);
+
+  [update_x]  move=3 & standstill<8 & (ski_position=3)  -> 0.4: (x'=max(minX,x-0)) & (move'=0) + 0.6: (x'=max(minX,x-1)) & (move'=0);
+  [update_x]  move=3 & standstill<8 & (ski_position=6)  -> 0.4: (x'=min(maxX,x+0)) & (move'=0) + 0.6: (x'=min(maxX,x+1)) & (move'=0);
+
+  [update_x]  move=3 & standstill<8 & (ski_position=2)  -> 0.3: (x'=max(minX,x-0)) & (move'=0) + 0.7: (x'=max(minX,x-1)) & (move'=0);
+  [update_x]  move=3 & standstill<8 & (ski_position=7)  -> 0.3: (x'=min(maxX,x+0)) & (move'=0) + 0.7: (x'=min(maxX,x+1)) & (move'=0);
+
+  [update_x]  move=3 & standstill<8 & (ski_position=1)  -> 0.2: (x'=max(minX,x-0)) & (move'=0) + 0.8: (x'=max(minX,x-1)) & (move'=0);
+  [update_x]  move=3 & standstill<8 & (ski_position=8)  -> 0.2: (x'=min(maxX,x+0)) & (move'=0) + 0.8: (x'=min(maxX,x+1)) & (move'=0);
+endmodule
+
+rewards
+  [left]  !done & (Hit_Tree) : -100;
+  [right] !done & (Hit_Tree) : -100;
+  [noop]  !done & (Hit_Tree) : -100;
+  [left]  !done & (Hit_Gate) : -100;
+  [right] !done & (Hit_Gate) : -100;
+  [noop]  !done & (Hit_Gate) : -100;
+  [done]  Unsafe : -100;
+endrewards
+