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