From 622338b7b0e6bba0fe26fddcd8152a7f1185bb6c Mon Sep 17 00:00:00 2001 From: sp Date: Wed, 8 May 2024 21:25:27 +0200 Subject: [PATCH] more tries with init mdp --- velocity_safety_no_formulas.prism | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/velocity_safety_no_formulas.prism b/velocity_safety_no_formulas.prism index f7f5985..02c7a5e 100644 --- a/velocity_safety_no_formulas.prism +++ b/velocity_safety_no_formulas.prism @@ -31,15 +31,15 @@ global move : [0..3]; module skier ski_position : [1..8] ; - done : bool ; + //done : bool ; - [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)); + [left] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); + [right] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position<8 -> (ski_position'=ski_position+1) & (move'=1); + [noop] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); - [done] Safe | Unsafe | done -> true; + [done] Safe | Unsafe | Hit_Tree | Hit_Gate -> true; endmodule module updateY @@ -74,12 +74,8 @@ module updateX 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; + Hit_Tree : -100; + Hit_Gate : -100; + Unsafe : -100; endrewards