From 812c42b105bf8ee6e449de21f8792fed6501d6cb Mon Sep 17 00:00:00 2001 From: sp Date: Tue, 7 May 2024 16:45:42 +0200 Subject: [PATCH] small update for init mdp --- velocity_safety_no_formulas.prism | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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;