From d7e1c14863782ff467f3d00bc33b14e8327f432e Mon Sep 17 00:00:00 2001
From: sp <stefan.pranger@iaik.tugraz.at>
Date: Thu, 9 May 2024 09:48:34 +0200
Subject: [PATCH] some fixes in init mdp

---
 velocity_safety_no_formulas.prism | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism
index 02c7a5e..73c0abb 100644
--- a/velocity_safety_no_formulas.prism
+++ b/velocity_safety_no_formulas.prism
@@ -9,10 +9,10 @@ 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_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);
 
 
@@ -30,8 +30,8 @@ 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 ;
+  ski_position : [1..8] init 4;
+  done : bool init false;
 
 
   [left]  !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1);
@@ -39,7 +39,7 @@ module skier
   [noop]  !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1);
 
 
-  [done] Safe | Unsafe | Hit_Tree | Hit_Gate -> true;
+  [done] move=0 & (Safe | Unsafe | Hit_Tree | Hit_Gate) -> (done'=true);
 endmodule
 
 module updateY
@@ -58,7 +58,7 @@ module updateY
 endmodule
 
 module updateX
-  x : [minX..maxX] ;
+  x : [minX..maxX] init initX;
 
   [update_x]  move=3 & standstill>=8                                       -> (move'=0);
   [update_x]  move=3 & standstill<8 & (ski_position=4 | ski_position=5)    -> (move'=0);
@@ -74,8 +74,8 @@ module updateX
 endmodule
 
 rewards
-  Hit_Tree : -100;
-  Hit_Gate : -100;
-  Unsafe : -100;
+  !done & Hit_Tree : -100;
+  !done & Hit_Gate : -100;
+  !done & Unsafe : -100;
 endrewards