|
|
@ -31,15 +31,15 @@ global move : [0..3]; |
|
|
|
|
|
|
|
|
module skier |
|
|
module skier |
|
|
ski_position : [1..8] ; |
|
|
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 |
|
|
endmodule |
|
|
|
|
|
|
|
|
module updateY |
|
|
module updateY |
|
|
@ -74,12 +74,8 @@ module updateX |
|
|
endmodule |
|
|
endmodule |
|
|
|
|
|
|
|
|
rewards |
|
|
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 |
|
|
endrewards |
|
|
|
|
|
|
