|
@ -30,8 +30,8 @@ formula Hit_Gate = Gate_1 | Gate_2 | Gate_3 | Gate_4 | Gate_5; |
|
|
global move : [0..3]; |
|
|
global move : [0..3]; |
|
|
|
|
|
|
|
|
module skier |
|
|
module skier |
|
|
ski_position : [1..8] ; |
|
|
|
|
|
//done : bool ; |
|
|
|
|
|
|
|
|
ski_position : [1..8] init 4; |
|
|
|
|
|
done : bool init false; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[left] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); |
|
|
[left] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 & ski_position>1 -> (ski_position'=ski_position-1) & (move'=1); |
|
@ -39,7 +39,7 @@ module skier |
|
|
[noop] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); |
|
|
[noop] !Safe & !Unsafe & !Hit_Gate & !Hit_Tree & move=0 -> (move'=1); |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
[done] Safe | Unsafe | Hit_Tree | Hit_Gate -> true; |
|
|
|
|
|
|
|
|
[done] move=0 & (Safe | Unsafe | Hit_Tree | Hit_Gate) -> (done'=true); |
|
|
endmodule |
|
|
endmodule |
|
|
|
|
|
|
|
|
module updateY |
|
|
module updateY |
|
@ -58,7 +58,7 @@ module updateY |
|
|
endmodule |
|
|
endmodule |
|
|
|
|
|
|
|
|
module updateX |
|
|
module updateX |
|
|
x : [minX..maxX] ; |
|
|
|
|
|
|
|
|
x : [minX..maxX] init initX; |
|
|
|
|
|
|
|
|
[update_x] move=3 & standstill>=8 -> (move'=0); |
|
|
[update_x] move=3 & standstill>=8 -> (move'=0); |
|
|
[update_x] move=3 & standstill<8 & (ski_position=4 | ski_position=5) -> (move'=0); |
|
|
[update_x] move=3 & standstill<8 & (ski_position=4 | ski_position=5) -> (move'=0); |
|
@ -74,8 +74,8 @@ module updateX |
|
|
endmodule |
|
|
endmodule |
|
|
|
|
|
|
|
|
rewards |
|
|
rewards |
|
|
Hit_Tree : -100; |
|
|
|
|
|
Hit_Gate : -100; |
|
|
|
|
|
Unsafe : -100; |
|
|
|
|
|
|
|
|
!done & Hit_Tree : -100; |
|
|
|
|
|
!done & Hit_Gate : -100; |
|
|
|
|
|
!done & Unsafe : -100; |
|
|
endrewards |
|
|
endrewards |
|
|
|
|
|
|