diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism index e49d30a..f7f5985 100644 --- a/velocity_safety_no_formulas.prism +++ b/velocity_safety_no_formulas.prism @@ -3,7 +3,8 @@ mdp const int initY = 40; const int initX = 80; -const int maxY = 580; +//const int maxY = 580; +const int maxY = 220; const int minX = 10; const int maxX = 144; @@ -33,9 +34,9 @@ module skier 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)); + [left] !Safe & !Unsafe & !done & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); + [right] !Safe & !Unsafe & !done & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1) & (done'=(Hit_Tree|Hit_Gate)); + [noop] !Safe & !Unsafe & !done & move=0 -> (move'=1) & (done'=(Hit_Tree|Hit_Gate)); [done] Safe | Unsafe | done -> true;