Browse Source

small update for init mdp

add_velocity_into_framework
sp 6 months ago
parent
commit
812c42b105
  1. 9
      velocity_safety_no_formulas.prism

9
velocity_safety_no_formulas.prism

@ -3,7 +3,8 @@ mdp
const int initY = 40; const int initY = 40;
const int initX = 80; const int initX = 80;
const int maxY = 580;
//const int maxY = 580;
const int maxY = 220;
const int minX = 10; const int minX = 10;
const int maxX = 144; const int maxX = 144;
@ -33,9 +34,9 @@ module skier
done : bool ; 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; [done] Safe | Unsafe | done -> true;

Loading…
Cancel
Save