sp
/
GSW_AI_LAB
Archived
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
The source code and dockerfile for the GSW2024 AI Lab.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
This repo is archived. You can view files and clone it, but cannot push or open issues/pull-requests.
16 Commits
1 Branch
0 Tags
27 MiB
Branch: main
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'main'
${ noResults }
GSW_AI_LAB/notebooks/environments/Minigrid/.ipynb_checkpoints/windy_adv-checkpoint.prism

386 lines
88 KiB
Raw Permalink Normal View History

initial commit
4 weeks ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
  1. smg
  3. formula AgentCannotMoveEastWall = (colAgent=13&rowAgent=1) | (colAgent=13&rowAgent=7) | (colAgent=13&rowAgent=8) | (colAgent=13&rowAgent=9);
  4. formula AgentCannotMoveNorthWall = (colAgent=13&rowAgent=1) | (colAgent=7&rowAgent=1) | (colAgent=8&rowAgent=1) | (colAgent=9&rowAgent=1) | (colAgent=10&rowAgent=1);
  5. formula AgentCannotMoveSouthWall = (colAgent=2&rowAgent=13);
  6. formula AgentCannotMoveWestWall = false;
  7. formula AgentIsOnSlipperyEast = (colAgent=7&rowAgent=3) | (colAgent=8&rowAgent=3) | (colAgent=9&rowAgent=3) | (colAgent=10&rowAgent=3) | (colAgent=4&rowAgent=4) | (colAgent=5&rowAgent=4) | (colAgent=4&rowAgent=6) | (colAgent=5&rowAgent=6) | (colAgent=11&rowAgent=6) | (colAgent=12&rowAgent=6) | (colAgent=13&rowAgent=6) | (colAgent=11&rowAgent=10) | (colAgent=12&rowAgent=10) | (colAgent=13&rowAgent=10) | (colAgent=4&rowAgent=12) | (colAgent=5&rowAgent=12);
  8. formula AgentIsOnSlipperyNorth = (colAgent=6&rowAgent=1) | (colAgent=11&rowAgent=1) | (colAgent=6&rowAgent=2) | (colAgent=11&rowAgent=2) | (colAgent=3&rowAgent=5) | (colAgent=6&rowAgent=5) | (colAgent=10&rowAgent=7) | (colAgent=10&rowAgent=8) | (colAgent=3&rowAgent=9) | (colAgent=6&rowAgent=9) | (colAgent=10&rowAgent=9) | (colAgent=3&rowAgent=10) | (colAgent=6&rowAgent=10) | (colAgent=3&rowAgent=11) | (colAgent=6&rowAgent=11);
  9. formula AgentIsOnSlipperyNorthEast = (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=4&rowAgent=1) | (colAgent=5&rowAgent=1) | (colAgent=12&rowAgent=1) | (colAgent=1&rowAgent=2) | (colAgent=2&rowAgent=2) | (colAgent=3&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=5&rowAgent=2) | (colAgent=12&rowAgent=2) | (colAgent=13&rowAgent=2) | (colAgent=1&rowAgent=3) | (colAgent=2&rowAgent=3) | (colAgent=3&rowAgent=3) | (colAgent=4&rowAgent=3) | (colAgent=5&rowAgent=3) | (colAgent=6&rowAgent=3) | (colAgent=11&rowAgent=3) | (colAgent=12&rowAgent=3) | (colAgent=13&rowAgent=3) | (colAgent=1&rowAgent=4) | (colAgent=2&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=6&rowAgent=4) | (colAgent=7&rowAgent=4) | (colAgent=8&rowAgent=4) | (colAgent=9&rowAgent=4) | (colAgent=10&rowAgent=4) | (colAgent=11&rowAgent=4) | (colAgent=12&rowAgent=4) | (colAgent=13&rowAgent=4) | (colAgent=1&rowAgent=5) | (colAgent=2&rowAgent=5) | (colAgent=7&rowAgent=5) | (colAgent=8&rowAgent=5) | (colAgent=9&rowAgent=5) | (colAgent=10&rowAgent=5) | (colAgent=11&rowAgent=5) | (colAgent=12&rowAgent=5) | (colAgent=13&rowAgent=5) | (colAgent=1&rowAgent=6) | (colAgent=2&rowAgent=6) | (colAgent=3&rowAgent=6) | (colAgent=6&rowAgent=6) | (colAgent=7&rowAgent=6) | (colAgent=9&rowAgent=6) | (colAgent=10&rowAgent=6) | (colAgent=1&rowAgent=7) | (colAgent=2&rowAgent=7) | (colAgent=3&rowAgent=7) | (colAgent=4&rowAgent=7) | (colAgent=6&rowAgent=7) | (colAgent=7&rowAgent=7) | (colAgent=8&rowAgent=7) | (colAgent=9&rowAgent=7) | (colAgent=1&rowAgent=8) | (colAgent=2&rowAgent=8) | (colAgent=3&rowAgent=8) | (colAgent=6&rowAgent=8) | (colAgent=7&rowAgent=8) | (colAgent=8&rowAgent=8) | (colAgent=9&rowAgent=8) | (colAgent=1&rowAgent=9) | (colAgent=2&rowAgent=9) | (colAgent=7&rowAgent=9) | (colAgent=8&rowAgent=9) | (colAgent=9&rowAgent=9) | (colAgent=1&rowAgent=10) | (colAgent=2&rowAgent=10) | (colAgent=7&rowAgent=10) | (colAgent=8&rowAgent=10) | (colAgent=9&rowAgent=10) | (colAgent=10&rowAgent=10) | (colAgent=1&rowAgent=11) | (colAgent=2&rowAgent=11) | (colAgent=7&rowAgent=11) | (colAgent=8&rowAgent=11) | (colAgent=9&rowAgent=11) | (colAgent=10&rowAgent=11) | (colAgent=11&rowAgent=11) | (colAgent=12&rowAgent=11) | (colAgent=13&rowAgent=11) | (colAgent=1&rowAgent=12) | (colAgent=2&rowAgent=12) | (colAgent=3&rowAgent=12) | (colAgent=6&rowAgent=12) | (colAgent=7&rowAgent=12) | (colAgent=8&rowAgent=12) | (colAgent=9&rowAgent=12) | (colAgent=10&rowAgent=12) | (colAgent=11&rowAgent=12) | (colAgent=12&rowAgent=12) | (colAgent=13&rowAgent=12) | (colAgent=1&rowAgent=13) | (colAgent=2&rowAgent=13) | (colAgent=3&rowAgent=13) | (colAgent=4&rowAgent=13) | (colAgent=5&rowAgent=13) | (colAgent=6&rowAgent=13) | (colAgent=7&rowAgent=13) | (colAgent=8&rowAgent=13) | (colAgent=9&rowAgent=13) | (colAgent=10&rowAgent=13) | (colAgent=11&rowAgent=13) | (colAgent=12&rowAgent=13) | (colAgent=13&rowAgent=13);
  10. formula AgentIsOnSlipperyNorthWest = false;
  11. formula AgentIsOnSlipperySouth = (colAgent=5&rowAgent=7) | (colAgent=5&rowAgent=8);
  12. formula AgentIsOnSlipperySouthEast = false;
  13. formula AgentIsOnSlipperySouthWest = false;
  14. formula AgentIsOnSlipperyWest = (colAgent=4&rowAgent=8);
  15. formula AgentIsOnSlippery = AgentIsOnSlipperyEast | AgentIsOnSlipperyNorth | AgentIsOnSlipperyNorthEast | AgentIsOnSlipperyNorthWest | AgentIsOnSlipperySouth | AgentIsOnSlipperySouthEast | AgentIsOnSlipperySouthWest | AgentIsOnSlipperyWest;
  16. formula AgentCannotSlipEast = (colAgent+1=0&rowAgent=0) | (colAgent+1=1&rowAgent=0) | (colAgent+1=2&rowAgent=0) | (colAgent+1=3&rowAgent=0) | (colAgent+1=4&rowAgent=0) | (colAgent+1=5&rowAgent=0) | (colAgent+1=6&rowAgent=0) | (colAgent+1=7&rowAgent=0) | (colAgent+1=8&rowAgent=0) | (colAgent+1=9&rowAgent=0) | (colAgent+1=10&rowAgent=0) | (colAgent+1=11&rowAgent=0) | (colAgent+1=12&rowAgent=0) | (colAgent+1=13&rowAgent=0) | (colAgent+1=14&rowAgent=0) | (colAgent+1=0&rowAgent=1) | (colAgent+1=14&rowAgent=1) | (colAgent+1=0&rowAgent=2) | (colAgent+1=14&rowAgent=2) | (colAgent+1=0&rowAgent=3) | (colAgent+1=14&rowAgent=3) | (colAgent+1=0&rowAgent=4) | (colAgent+1=14&rowAgent=4) | (colAgent+1=0&rowAgent=5) | (colAgent+1=14&rowAgent=5) | (colAgent+1=0&rowAgent=6) | (colAgent+1=14&rowAgent=6) | (colAgent+1=0&rowAgent=7) | (colAgent+1=14&rowAgent=7) | (colAgent+1=0&rowAgent=8) | (colAgent+1=14&rowAgent=8) | (colAgent+1=0&rowAgent=9) | (colAgent+1=14&rowAgent=9) | (colAgent+1=0&rowAgent=10) | (colAgent+1=14&rowAgent=10) | (colAgent+1=0&rowAgent=11) | (colAgent+1=14&rowAgent=11) | (colAgent+1=0&rowAgent=12) | (colAgent+1=14&rowAgent=12) | (colAgent+1=0&rowAgent=13) | (colAgent+1=14&rowAgent=13) | (colAgent+1=0&rowAgent=14) | (colAgent+1=1&rowAgent=14) | (colAgent+1=2&rowAgent=14) | (colAgent+1=3&rowAgent=14) | (colAgent+1=4&rowAgent=14) | (colAgent+1=5&rowAgent=14) | (colAgent+1=6&rowAgent=14) | (colAgent+1=7&rowAgent=14) | (colAgent+1=8&rowAgent=14) | (colAgent+1=9&rowAgent=14) | (colAgent+1=10&rowAgent=14) | (colAgent+1=11&rowAgent=14) | (colAgent+1=12&rowAgent=14) | (colAgent+1=13&rowAgent=14) | (colAgent+1=14&rowAgent=14);
  17. formula AgentCannotSlipNorth = (colAgent=0&rowAgent-1=0) | (colAgent=1&rowAgent-1=0) | (colAgent=2&rowAgent-1=0) | (colAgent=3&rowAgent-1=0) | (colAgent=4&rowAgent-1=0) | (colAgent=5&rowAgent-1=0) | (colAgent=6&rowAgent-1=0) | (colAgent=7&rowAgent-1=0) | (colAgent=8&rowAgent-1=0) | (colAgent=9&rowAgent-1=0) | (colAgent=10&rowAgent-1=0) | (colAgent=11&rowAgent-1=0) | (colAgent=12&rowAgent-1=0) | (colAgent=13&rowAgent-1=0) | (colAgent=14&rowAgent-1=0) | (colAgent=0&rowAgent-1=1) | (colAgent=14&rowAgent-1=1) | (colAgent=0&rowAgent-1=2) | (colAgent=14&rowAgent-1=2) | (colAgent=0&rowAgent-1=3) | (colAgent=14&rowAgent-1=3) | (colAgent=0&rowAgent-1=4) | (colAgent=14&rowAgent-1=4) | (colAgent=0&rowAgent-1=5) | (colAgent=14&rowAgent-1=5) | (colAgent=0&rowAgent-1=6) | (colAgent=14&rowAgent-1=6) | (colAgent=0&rowAgent-1=7) | (colAgent=14&rowAgent-1=7) | (colAgent=0&rowAgent-1=8) | (colAgent=14&rowAgent-1=8) | (colAgent=0&rowAgent-1=9) | (colAgent=14&rowAgent-1=9) | (colAgent=0&rowAgent-1=10) | (colAgent=14&rowAgent-1=10) | (colAgent=0&rowAgent-1=11) | (colAgent=14&rowAgent-1=11) | (colAgent=0&rowAgent-1=12) | (colAgent=14&rowAgent-1=12) | (colAgent=0&rowAgent-1=13) | (colAgent=14&rowAgent-1=13) | (colAgent=0&rowAgent-1=14) | (colAgent=1&rowAgent-1=14) | (colAgent=2&rowAgent-1=14) | (colAgent=3&rowAgent-1=14) | (colAgent=4&rowAgent-1=14) | (colAgent=5&rowAgent-1=14) | (colAgent=6&rowAgent-1=14) | (colAgent=7&rowAgent-1=14) | (colAgent=8&rowAgent-1=14) | (colAgent=9&rowAgent-1=14) | (colAgent=10&rowAgent-1=14) | (colAgent=11&rowAgent-1=14) | (colAgent=12&rowAgent-1=14) | (colAgent=13&rowAgent-1=14) | (colAgent=14&rowAgent-1=14);
  18. formula AgentCannotSlipNorthEast = (colAgent+1=0&rowAgent-1=0) | (colAgent+1=1&rowAgent-1=0) | (colAgent+1=2&rowAgent-1=0) | (colAgent+1=3&rowAgent-1=0) | (colAgent+1=4&rowAgent-1=0) | (colAgent+1=5&rowAgent-1=0) | (colAgent+1=6&rowAgent-1=0) | (colAgent+1=7&rowAgent-1=0) | (colAgent+1=8&rowAgent-1=0) | (colAgent+1=9&rowAgent-1=0) | (colAgent+1=10&rowAgent-1=0) | (colAgent+1=11&rowAgent-1=0) | (colAgent+1=12&rowAgent-1=0) | (colAgent+1=13&rowAgent-1=0) | (colAgent+1=14&rowAgent-1=0) | (colAgent+1=0&rowAgent-1=1) | (colAgent+1=14&rowAgent-1=1) | (colAgent+1=0&rowAgent-1=2) | (colAgent+1=14&rowAgent-1=2) | (colAgent+1=0&rowAgent-1=3) | (colAgent+1=14&rowAgent-1=3) | (colAgent+1=0&rowAgent-1=4) | (colAgent+1=14&rowAgent-1=4) | (colAgent+1=0&rowAgent-1=5) | (colAgent+1=14&rowAgent-1=5) | (colAgent+1=0&rowAgent-1=6) | (colAgent+1=14&rowAgent-1=6) | (colAgent+1=0&rowAgent-1=7) | (colAgent+1=14&rowAgent-1=7) | (colAgent+1=0&rowAgent-1=8) | (colAgent+1=14&rowAgent-1=8) | (colAgent+1=0&rowAgent-1=9) | (colAgent+1=14&rowAgent-1=9) | (colAgent+1=0&rowAgent-1=10) | (colAgent+1=14&rowAgent-1=10) | (colAgent+1=0&rowAgent-1=11) | (colAgent+1=14&rowAgent-1=11) | (colAgent+1=0&rowAgent-1=12) | (colAgent+1=14&rowAgent-1=12) | (colAgent+1=0&rowAgent-1=13) | (colAgent+1=14&rowAgent-1=13) | (colAgent+1=0&rowAgent-1=14) | (colAgent+1=1&rowAgent-1=14) | (colAgent+1=2&rowAgent-1=14) | (colAgent+1=3&rowAgent-1=14) | (colAgent+1=4&rowAgent-1=14) | (colAgent+1=5&rowAgent-1=14) | (colAgent+1=6&rowAgent-1=14) | (colAgent+1=7&rowAgent-1=14) | (colAgent+1=8&rowAgent-1=14) | (colAgent+1=9&rowAgent-1=14) | (colAgent+1=10&rowAgent-1=14) | (colAgent+1=11&rowAgent-1=14) | (colAgent+1=12&rowAgent-1=14) | (colAgent+1=13&rowAgent-1=14) | (colAgent+1=14&rowAgent-1=14);
  19. formula AgentCannotSlipNorthWest = (colAgent-1=0&rowAgent-1=0) | (colAgent-1=1&rowAgent-1=0) | (colAgent-1=2&rowAgent-1=0) | (colAgent-1=3&rowAgent-1=0) | (colAgent-1=4&rowAgent-1=0) | (colAgent-1=5&rowAgent-1=0) | (colAgent-1=6&rowAgent-1=0) | (colAgent-1=7&rowAgent-1=0) | (colAgent-1=8&rowAgent-1=0) | (colAgent-1=9&rowAgent-1=0) | (colAgent-1=10&rowAgent-1=0) | (colAgent-1=11&rowAgent-1=0) | (colAgent-1=12&rowAgent-1=0) | (colAgent-1=13&rowAgent-1=0) | (colAgent-1=14&rowAgent-1=0) | (colAgent-1=0&rowAgent-1=1) | (colAgent-1=14&rowAgent-1=1) | (colAgent-1=0&rowAgent-1=2) | (colAgent-1=14&rowAgent-1=2) | (colAgent-1=0&rowAgent-1=3) | (colAgent-1=14&rowAgent-1=3) | (colAgent-1=0&rowAgent-1=4) | (colAgent-1=14&rowAgent-1=4) | (colAgent-1=0&rowAgent-1=5) | (colAgent-1=14&rowAgent-1=5) | (colAgent-1=0&rowAgent-1=6) | (colAgent-1=14&rowAgent-1=6) | (colAgent-1=0&rowAgent-1=7) | (colAgent-1=14&rowAgent-1=7) | (colAgent-1=0&rowAgent-1=8) | (colAgent-1=14&rowAgent-1=8) | (colAgent-1=0&rowAgent-1=9) | (colAgent-1=14&rowAgent-1=9) | (colAgent-1=0&rowAgent-1=10) | (colAgent-1=14&rowAgent-1=10) | (colAgent-1=0&rowAgent-1=11) | (colAgent-1=14&rowAgent-1=11) | (colAgent-1=0&rowAgent-1=12) | (colAgent-1=14&rowAgent-1=12) | (colAgent-1=0&rowAgent-1=13) | (colAgent-1=14&rowAgent-1=13) | (colAgent-1=0&rowAgent-1=14) | (colAgent-1=1&rowAgent-1=14) | (colAgent-1=2&rowAgent-1=14) | (colAgent-1=3&rowAgent-1=14) | (colAgent-1=4&rowAgent-1=14) | (colAgent-1=5&rowAgent-1=14) | (colAgent-1=6&rowAgent-1=14) | (colAgent-1=7&rowAgent-1=14) | (colAgent-1=8&rowAgent-1=14) | (colAgent-1=9&rowAgent-1=14) | (colAgent-1=10&rowAgent-1=14) | (colAgent-1=11&rowAgent-1=14) | (colAgent-1=12&rowAgent-1=14) | (colAgent-1=13&rowAgent-1=14) | (colAgent-1=14&rowAgent-1=14);
  20. formula AgentCannotSlipSouth = (colAgent=0&rowAgent+1=0) | (colAgent=1&rowAgent+1=0) | (colAgent=2&rowAgent+1=0) | (colAgent=3&rowAgent+1=0) | (colAgent=4&rowAgent+1=0) | (colAgent=5&rowAgent+1=0) | (colAgent=6&rowAgent+1=0) | (colAgent=7&rowAgent+1=0) | (colAgent=8&rowAgent+1=0) | (colAgent=9&rowAgent+1=0) | (colAgent=10&rowAgent+1=0) | (colAgent=11&rowAgent+1=0) | (colAgent=12&rowAgent+1=0) | (colAgent=13&rowAgent+1=0) | (colAgent=14&rowAgent+1=0) | (colAgent=0&rowAgent+1=1) | (colAgent=14&rowAgent+1=1) | (colAgent=0&rowAgent+1=2) | (colAgent=14&rowAgent+1=2) | (colAgent=0&rowAgent+1=3) | (colAgent=14&rowAgent+1=3) | (colAgent=0&rowAgent+1=4) | (colAgent=14&rowAgent+1=4) | (colAgent=0&rowAgent+1=5) | (colAgent=14&rowAgent+1=5) | (colAgent=0&rowAgent+1=6) | (colAgent=14&rowAgent+1=6) | (colAgent=0&rowAgent+1=7) | (colAgent=14&rowAgent+1=7) | (colAgent=0&rowAgent+1=8) | (colAgent=14&rowAgent+1=8) | (colAgent=0&rowAgent+1=9) | (colAgent=14&rowAgent+1=9) | (colAgent=0&rowAgent+1=10) | (colAgent=14&rowAgent+1=10) | (colAgent=0&rowAgent+1=11) | (colAgent=14&rowAgent+1=11) | (colAgent=0&rowAgent+1=12) | (colAgent=14&rowAgent+1=12) | (colAgent=0&rowAgent+1=13) | (colAgent=14&rowAgent+1=13) | (colAgent=0&rowAgent+1=14) | (colAgent=1&rowAgent+1=14) | (colAgent=2&rowAgent+1=14) | (colAgent=3&rowAgent+1=14) | (colAgent=4&rowAgent+1=14) | (colAgent=5&rowAgent+1=14) | (colAgent=6&rowAgent+1=14) | (colAgent=7&rowAgent+1=14) | (colAgent=8&rowAgent+1=14) | (colAgent=9&rowAgent+1=14) | (colAgent=10&rowAgent+1=14) | (colAgent=11&rowAgent+1=14) | (colAgent=12&rowAgent+1=14) | (colAgent=13&rowAgent+1=14) | (colAgent=14&rowAgent+1=14);
  21. formula AgentCannotSlipSouthEast = (colAgent+1=0&rowAgent+1=0) | (colAgent+1=1&rowAgent+1=0) | (colAgent+1=2&rowAgent+1=0) | (colAgent+1=3&rowAgent+1=0) | (colAgent+1=4&rowAgent+1=0) | (colAgent+1=5&rowAgent+1=0) | (colAgent+1=6&rowAgent+1=0) | (colAgent+1=7&rowAgent+1=0) | (colAgent+1=8&rowAgent+1=0) | (colAgent+1=9&rowAgent+1=0) | (colAgent+1=10&rowAgent+1=0) | (colAgent+1=11&rowAgent+1=0) | (colAgent+1=12&rowAgent+1=0) | (colAgent+1=13&rowAgent+1=0) | (colAgent+1=14&rowAgent+1=0) | (colAgent+1=0&rowAgent+1=1) | (colAgent+1=14&rowAgent+1=1) | (colAgent+1=0&rowAgent+1=2) | (colAgent+1=14&rowAgent+1=2) | (colAgent+1=0&rowAgent+1=3) | (colAgent+1=14&rowAgent+1=3) | (colAgent+1=0&rowAgent+1=4) | (colAgent+1=14&rowAgent+1=4) | (colAgent+1=0&rowAgent+1=5) | (colAgent+1=14&rowAgent+1=5) | (colAgent+1=0&rowAgent+1=6) | (colAgent+1=14&rowAgent+1=6) | (colAgent+1=0&rowAgent+1=7) | (colAgent+1=14&rowAgent+1=7) | (colAgent+1=0&rowAgent+1=8) | (colAgent+1=14&rowAgent+1=8) | (colAgent+1=0&rowAgent+1=9) | (colAgent+1=14&rowAgent+1=9) | (colAgent+1=0&rowAgent+1=10) | (colAgent+1=14&rowAgent+1=10) | (colAgent+1=0&rowAgent+1=11) | (colAgent+1=14&rowAgent+1=11) | (colAgent+1=0&rowAgent+1=12) | (colAgent+1=14&rowAgent+1=12) | (colAgent+1=0&rowAgent+1=13) | (colAgent+1=14&rowAgent+1=13) | (colAgent+1=0&rowAgent+1=14) | (colAgent+1=1&rowAgent+1=14) | (colAgent+1=2&rowAgent+1=14) | (colAgent+1=3&rowAgent+1=14) | (colAgent+1=4&rowAgent+1=14) | (colAgent+1=5&rowAgent+1=14) | (colAgent+1=6&rowAgent+1=14) | (colAgent+1=7&rowAgent+1=14) | (colAgent+1=8&rowAgent+1=14) | (colAgent+1=9&rowAgent+1=14) | (colAgent+1=10&rowAgent+1=14) | (colAgent+1=11&rowAgent+1=14) | (colAgent+1=12&rowAgent+1=14) | (colAgent+1=13&rowAgent+1=14) | (colAgent+1=14&rowAgent+1=14);
  22. formula AgentCannotSlipSouthWest = (colAgent-1=0&rowAgent+1=0) | (colAgent-1=1&rowAgent+1=0) | (colAgent-1=2&rowAgent+1=0) | (colAgent-1=3&rowAgent+1=0) | (colAgent-1=4&rowAgent+1=0) | (colAgent-1=5&rowAgent+1=0) | (colAgent-1=6&rowAgent+1=0) | (colAgent-1=7&rowAgent+1=0) | (colAgent-1=8&rowAgent+1=0) | (colAgent-1=9&rowAgent+1=0) | (colAgent-1=10&rowAgent+1=0) | (colAgent-1=11&rowAgent+1=0) | (colAgent-1=12&rowAgent+1=0) | (colAgent-1=13&rowAgent+1=0) | (colAgent-1=14&rowAgent+1=0) | (colAgent-1=0&rowAgent+1=1) | (colAgent-1=14&rowAgent+1=1) | (colAgent-1=0&rowAgent+1=2) | (colAgent-1=14&rowAgent+1=2) | (colAgent-1=0&rowAgent+1=3) | (colAgent-1=14&rowAgent+1=3) | (colAgent-1=0&rowAgent+1=4) | (colAgent-1=14&rowAgent+1=4) | (colAgent-1=0&rowAgent+1=5) | (colAgent-1=14&rowAgent+1=5) | (colAgent-1=0&rowAgent+1=6) | (colAgent-1=14&rowAgent+1=6) | (colAgent-1=0&rowAgent+1=7) | (colAgent-1=14&rowAgent+1=7) | (colAgent-1=0&rowAgent+1=8) | (colAgent-1=14&rowAgent+1=8) | (colAgent-1=0&rowAgent+1=9) | (colAgent-1=14&rowAgent+1=9) | (colAgent-1=0&rowAgent+1=10) | (colAgent-1=14&rowAgent+1=10) | (colAgent-1=0&rowAgent+1=11) | (colAgent-1=14&rowAgent+1=11) | (colAgent-1=0&rowAgent+1=12) | (colAgent-1=14&rowAgent+1=12) | (colAgent-1=0&rowAgent+1=13) | (colAgent-1=14&rowAgent+1=13) | (colAgent-1=0&rowAgent+1=14) | (colAgent-1=1&rowAgent+1=14) | (colAgent-1=2&rowAgent+1=14) | (colAgent-1=3&rowAgent+1=14) | (colAgent-1=4&rowAgent+1=14) | (colAgent-1=5&rowAgent+1=14) | (colAgent-1=6&rowAgent+1=14) | (colAgent-1=7&rowAgent+1=14) | (colAgent-1=8&rowAgent+1=14) | (colAgent-1=9&rowAgent+1=14) | (colAgent-1=10&rowAgent+1=14) | (colAgent-1=11&rowAgent+1=14) | (colAgent-1=12&rowAgent+1=14) | (colAgent-1=13&rowAgent+1=14) | (colAgent-1=14&rowAgent+1=14);
  23. formula AgentCannotSlipWest = (colAgent-1=0&rowAgent=0) | (colAgent-1=1&rowAgent=0) | (colAgent-1=2&rowAgent=0) | (colAgent-1=3&rowAgent=0) | (colAgent-1=4&rowAgent=0) | (colAgent-1=5&rowAgent=0) | (colAgent-1=6&rowAgent=0) | (colAgent-1=7&rowAgent=0) | (colAgent-1=8&rowAgent=0) | (colAgent-1=9&rowAgent=0) | (colAgent-1=10&rowAgent=0) | (colAgent-1=11&rowAgent=0) | (colAgent-1=12&rowAgent=0) | (colAgent-1=13&rowAgent=0) | (colAgent-1=14&rowAgent=0) | (colAgent-1=0&rowAgent=1) | (colAgent-1=14&rowAgent=1) | (colAgent-1=0&rowAgent=2) | (colAgent-1=14&rowAgent=2) | (colAgent-1=0&rowAgent=3) | (colAgent-1=14&rowAgent=3) | (colAgent-1=0&rowAgent=4) | (colAgent-1=14&rowAgent=4) | (colAgent-1=0&rowAgent=5) | (colAgent-1=14&rowAgent=5) | (colAgent-1=0&rowAgent=6) | (colAgent-1=14&rowAgent=6) | (colAgent-1=0&rowAgent=7) | (colAgent-1=14&rowAgent=7) | (colAgent-1=0&rowAgent=8) | (colAgent-1=14&rowAgent=8) | (colAgent-1=0&rowAgent=9) | (colAgent-1=14&rowAgent=9) | (colAgent-1=0&rowAgent=10) | (colAgent-1=14&rowAgent=10) | (colAgent-1=0&rowAgent=11) | (colAgent-1=14&rowAgent=11) | (colAgent-1=0&rowAgent=12) | (colAgent-1=14&rowAgent=12) | (colAgent-1=0&rowAgent=13) | (colAgent-1=14&rowAgent=13) | (colAgent-1=0&rowAgent=14) | (colAgent-1=1&rowAgent=14) | (colAgent-1=2&rowAgent=14) | (colAgent-1=3&rowAgent=14) | (colAgent-1=4&rowAgent=14) | (colAgent-1=5&rowAgent=14) | (colAgent-1=6&rowAgent=14) | (colAgent-1=7&rowAgent=14) | (colAgent-1=8&rowAgent=14) | (colAgent-1=9&rowAgent=14) | (colAgent-1=10&rowAgent=14) | (colAgent-1=11&rowAgent=14) | (colAgent-1=12&rowAgent=14) | (colAgent-1=13&rowAgent=14) | (colAgent-1=14&rowAgent=14);
  24. formula AgentIsOnLava = (colAgent=7&rowAgent=1) | (colAgent=8&rowAgent=1) | (colAgent=9&rowAgent=1) | (colAgent=10&rowAgent=1) | (colAgent=7&rowAgent=2) | (colAgent=8&rowAgent=2) | (colAgent=9&rowAgent=2) | (colAgent=10&rowAgent=2) | (colAgent=4&rowAgent=5) | (colAgent=5&rowAgent=5) | (colAgent=11&rowAgent=7) | (colAgent=12&rowAgent=7) | (colAgent=13&rowAgent=7) | (colAgent=11&rowAgent=8) | (colAgent=12&rowAgent=8) | (colAgent=13&rowAgent=8) | (colAgent=4&rowAgent=9) | (colAgent=5&rowAgent=9) | (colAgent=11&rowAgent=9) | (colAgent=12&rowAgent=9) | (colAgent=13&rowAgent=9) | (colAgent=4&rowAgent=10) | (colAgent=5&rowAgent=10) | (colAgent=4&rowAgent=11) | (colAgent=5&rowAgent=11);
  25. formula AgentIsOnGoal = (colAgent=13&rowAgent=1);
  26. formula BlueCannotMoveEastWall = (colBlue=13&rowBlue=1) | (colBlue=13&rowBlue=7) | (colBlue=13&rowBlue=8) | (colBlue=13&rowBlue=9);
  27. formula BlueCannotMoveNorthWall = (colBlue=13&rowBlue=1) | (colBlue=7&rowBlue=1) | (colBlue=8&rowBlue=1) | (colBlue=9&rowBlue=1) | (colBlue=10&rowBlue=1);
  28. formula BlueCannotMoveSouthWall = (colBlue=2&rowBlue=13);
  29. formula BlueCannotMoveWestWall = false;
  30. formula BlueIsOnSlipperyEast = (colBlue=7&rowBlue=3) | (colBlue=8&rowBlue=3) | (colBlue=9&rowBlue=3) | (colBlue=10&rowBlue=3) | (colBlue=4&rowBlue=4) | (colBlue=5&rowBlue=4) | (colBlue=4&rowBlue=6) | (colBlue=5&rowBlue=6) | (colBlue=11&rowBlue=6) | (colBlue=12&rowBlue=6) | (colBlue=13&rowBlue=6) | (colBlue=11&rowBlue=10) | (colBlue=12&rowBlue=10) | (colBlue=13&rowBlue=10) | (colBlue=4&rowBlue=12) | (colBlue=5&rowBlue=12);
  31. formula BlueIsOnSlipperyNorth = (colBlue=6&rowBlue=1) | (colBlue=11&rowBlue=1) | (colBlue=6&rowBlue=2) | (colBlue=11&rowBlue=2) | (colBlue=3&rowBlue=5) | (colBlue=6&rowBlue=5) | (colBlue=10&rowBlue=7) | (colBlue=10&rowBlue=8) | (colBlue=3&rowBlue=9) | (colBlue=6&rowBlue=9) | (colBlue=10&rowBlue=9) | (colBlue=3&rowBlue=10) | (colBlue=6&rowBlue=10) | (colBlue=3&rowBlue=11) | (colBlue=6&rowBlue=11);
  32. formula BlueIsOnSlipperyNorthEast = (colBlue=1&rowBlue=1) | (colBlue=2&rowBlue=1) | (colBlue=3&rowBlue=1) | (colBlue=4&rowBlue=1) | (colBlue=5&rowBlue=1) | (colBlue=12&rowBlue=1) | (colBlue=1&rowBlue=2) | (colBlue=2&rowBlue=2) | (colBlue=3&rowBlue=2) | (colBlue=4&rowBlue=2) | (colBlue=5&rowBlue=2) | (colBlue=12&rowBlue=2) | (colBlue=13&rowBlue=2) | (colBlue=1&rowBlue=3) | (colBlue=2&rowBlue=3) | (colBlue=3&rowBlue=3) | (colBlue=4&rowBlue=3) | (colBlue=5&rowBlue=3) | (colBlue=6&rowBlue=3) | (colBlue=11&rowBlue=3) | (colBlue=12&rowBlue=3) | (colBlue=13&rowBlue=3) | (colBlue=1&rowBlue=4) | (colBlue=2&rowBlue=4) | (colBlue=3&rowBlue=4) | (colBlue=6&rowBlue=4) | (colBlue=7&rowBlue=4) | (colBlue=8&rowBlue=4) | (colBlue=9&rowBlue=4) | (colBlue=10&rowBlue=4) | (colBlue=11&rowBlue=4) | (colBlue=12&rowBlue=4) | (colBlue=13&rowBlue=4) | (colBlue=1&rowBlue=5) | (colBlue=2&rowBlue=5) | (colBlue=7&rowBlue=5) | (colBlue=8&rowBlue=5) | (colBlue=9&rowBlue=5) | (colBlue=10&rowBlue=5) | (colBlue=11&rowBlue=5) | (colBlue=12&rowBlue=5) | (colBlue=13&rowBlue=5) | (colBlue=1&rowBlue=6) | (colBlue=2&rowBlue=6) | (colBlue=3&rowBlue=6) | (colBlue=6&rowBlue=6) | (colBlue=7&rowBlue=6) | (colBlue=9&rowBlue=6) | (colBlue=10&rowBlue=6) | (colBlue=1&rowBlue=7) | (colBlue=2&rowBlue=7) | (colBlue=3&rowBlue=7) | (colBlue=4&rowBlue=7) | (colBlue=6&rowBlue=7) | (colBlue=7&rowBlue=7) | (colBlue=8&rowBlue=7) | (colBlue=9&rowBlue=7) | (colBlue=1&rowBlue=8) | (colBlue=2&rowBlue=8) | (colBlue=3&rowBlue=8) | (colBlue=6&rowBlue=8) | (colBlue=7&rowBlue=8) | (colBlue=8&rowBlue=8) | (colBlue=9&rowBlue=8) | (colBlue=1&rowBlue=9) | (colBlue=2&rowBlue=9) | (colBlue=7&rowBlue=9) | (colBlue=8&rowBlue=9) | (colBlue=9&rowBlue=9) | (colBlue=1&rowBlue=10) | (colBlue=2&rowBlue=10) | (colBlue=7&rowBlue=10) | (colBlue=8&rowBlue=10) | (colBlue=9&rowBlue=10) | (colBlue=10&rowBlue=10) | (colBlue=1&rowBlue=11) | (colBlue=2&rowBlue=11) | (colBlue=7&rowBlue=11) | (colBlue=8&rowBlue=11) | (colBlue=9&rowBlue=11) | (colBlue=10&rowBlue=11) | (colBlue=11&rowBlue=11) | (colBlue=12&rowBlue=11) | (colBlue=13&rowBlue=11) | (colBlue=1&rowBlue=12) | (colBlue=2&rowBlue=12) | (colBlue=3&rowBlue=12) | (colBlue=6&rowBlue=12) | (colBlue=7&rowBlue=12) | (colBlue=8&rowBlue=12) | (colBlue=9&rowBlue=12) | (colBlue=10&rowBlue=12) | (colBlue=11&rowBlue=12) | (colBlue=12&rowBlue=12) | (colBlue=13&rowBlue=12) | (colBlue=1&rowBlue=13) | (colBlue=2&rowBlue=13) | (colBlue=3&rowBlue=13) | (colBlue=4&rowBlue=13) | (colBlue=5&rowBlue=13) | (colBlue=6&rowBlue=13) | (colBlue=7&rowBlue=13) | (colBlue=8&rowBlue=13) | (colBlue=9&rowBlue=13) | (colBlue=10&rowBlue=13) | (colBlue=11&rowBlue=13) | (colBlue=12&rowBlue=13) | (colBlue=13&rowBlue=13);
  33. formula BlueIsOnSlipperyNorthWest = false;
  34. formula BlueIsOnSlipperySouth = (colBlue=5&rowBlue=7) | (colBlue=5&rowBlue=8);
  35. formula BlueIsOnSlipperySouthEast = false;
  36. formula BlueIsOnSlipperySouthWest = false;
  37. formula BlueIsOnSlipperyWest = (colBlue=4&rowBlue=8);
  38. formula BlueIsOnSlippery = BlueIsOnSlipperyEast | BlueIsOnSlipperyNorth | BlueIsOnSlipperyNorthEast | BlueIsOnSlipperyNorthWest | BlueIsOnSlipperySouth | BlueIsOnSlipperySouthEast | BlueIsOnSlipperySouthWest | BlueIsOnSlipperyWest;
  39. formula BlueCannotSlipEast = (colBlue+1=0&rowBlue=0) | (colBlue+1=1&rowBlue=0) | (colBlue+1=2&rowBlue=0) | (colBlue+1=3&rowBlue=0) | (colBlue+1=4&rowBlue=0) | (colBlue+1=5&rowBlue=0) | (colBlue+1=6&rowBlue=0) | (colBlue+1=7&rowBlue=0) | (colBlue+1=8&rowBlue=0) | (colBlue+1=9&rowBlue=0) | (colBlue+1=10&rowBlue=0) | (colBlue+1=11&rowBlue=0) | (colBlue+1=12&rowBlue=0) | (colBlue+1=13&rowBlue=0) | (colBlue+1=14&rowBlue=0) | (colBlue+1=0&rowBlue=1) | (colBlue+1=14&rowBlue=1) | (colBlue+1=0&rowBlue=2) | (colBlue+1=14&rowBlue=2) | (colBlue+1=0&rowBlue=3) | (colBlue+1=14&rowBlue=3) | (colBlue+1=0&rowBlue=4) | (colBlue+1=14&rowBlue=4) | (colBlue+1=0&rowBlue=5) | (colBlue+1=14&rowBlue=5) | (colBlue+1=0&rowBlue=6) | (colBlue+1=14&rowBlue=6) | (colBlue+1=0&rowBlue=7) | (colBlue+1=14&rowBlue=7) | (colBlue+1=0&rowBlue=8) | (colBlue+1=14&rowBlue=8) | (colBlue+1=0&rowBlue=9) | (colBlue+1=14&rowBlue=9) | (colBlue+1=0&rowBlue=10) | (colBlue+1=14&rowBlue=10) | (colBlue+1=0&rowBlue=11) | (colBlue+1=14&rowBlue=11) | (colBlue+1=0&rowBlue=12) | (colBlue+1=14&rowBlue=12) | (colBlue+1=0&rowBlue=13) | (colBlue+1=14&rowBlue=13) | (colBlue+1=0&rowBlue=14) | (colBlue+1=1&rowBlue=14) | (colBlue+1=2&rowBlue=14) | (colBlue+1=3&rowBlue=14) | (colBlue+1=4&rowBlue=14) | (colBlue+1=5&rowBlue=14) | (colBlue+1=6&rowBlue=14) | (colBlue+1=7&rowBlue=14) | (colBlue+1=8&rowBlue=14) | (colBlue+1=9&rowBlue=14) | (colBlue+1=10&rowBlue=14) | (colBlue+1=11&rowBlue=14) | (colBlue+1=12&rowBlue=14) | (colBlue+1=13&rowBlue=14) | (colBlue+1=14&rowBlue=14);
  40. formula BlueCannotSlipNorth = (colBlue=0&rowBlue-1=0) | (colBlue=1&rowBlue-1=0) | (colBlue=2&rowBlue-1=0) | (colBlue=3&rowBlue-1=0) | (colBlue=4&rowBlue-1=0) | (colBlue=5&rowBlue-1=0) | (colBlue=6&rowBlue-1=0) | (colBlue=7&rowBlue-1=0) | (colBlue=8&rowBlue-1=0) | (colBlue=9&rowBlue-1=0) | (colBlue=10&rowBlue-1=0) | (colBlue=11&rowBlue-1=0) | (colBlue=12&rowBlue-1=0) | (colBlue=13&rowBlue-1=0) | (colBlue=14&rowBlue-1=0) | (colBlue=0&rowBlue-1=1) | (colBlue=14&rowBlue-1=1) | (colBlue=0&rowBlue-1=2) | (colBlue=14&rowBlue-1=2) | (colBlue=0&rowBlue-1=3) | (colBlue=14&rowBlue-1=3) | (colBlue=0&rowBlue-1=4) | (colBlue=14&rowBlue-1=4) | (colBlue=0&rowBlue-1=5) | (colBlue=14&rowBlue-1=5) | (colBlue=0&rowBlue-1=6) | (colBlue=14&rowBlue-1=6) | (colBlue=0&rowBlue-1=7) | (colBlue=14&rowBlue-1=7) | (colBlue=0&rowBlue-1=8) | (colBlue=14&rowBlue-1=8) | (colBlue=0&rowBlue-1=9) | (colBlue=14&rowBlue-1=9) | (colBlue=0&rowBlue-1=10) | (colBlue=14&rowBlue-1=10) | (colBlue=0&rowBlue-1=11) | (colBlue=14&rowBlue-1=11) | (colBlue=0&rowBlue-1=12) | (colBlue=14&rowBlue-1=12) | (colBlue=0&rowBlue-1=13) | (colBlue=14&rowBlue-1=13) | (colBlue=0&rowBlue-1=14) | (colBlue=1&rowBlue-1=14) | (colBlue=2&rowBlue-1=14) | (colBlue=3&rowBlue-1=14) | (colBlue=4&rowBlue-1=14) | (colBlue=5&rowBlue-1=14) | (colBlue=6&rowBlue-1=14) | (colBlue=7&rowBlue-1=14) | (colBlue=8&rowBlue-1=14) | (colBlue=9&rowBlue-1=14) | (colBlue=10&rowBlue-1=14) | (colBlue=11&rowBlue-1=14) | (colBlue=12&rowBlue-1=14) | (colBlue=13&rowBlue-1=14) | (colBlue=14&rowBlue-1=14);
  41. formula BlueCannotSlipNorthEast = (colBlue+1=0&rowBlue-1=0) | (colBlue+1=1&rowBlue-1=0) | (colBlue+1=2&rowBlue-1=0) | (colBlue+1=3&rowBlue-1=0) | (colBlue+1=4&rowBlue-1=0) | (colBlue+1=5&rowBlue-1=0) | (colBlue+1=6&rowBlue-1=0) | (colBlue+1=7&rowBlue-1=0) | (colBlue+1=8&rowBlue-1=0) | (colBlue+1=9&rowBlue-1=0) | (colBlue+1=10&rowBlue-1=0) | (colBlue+1=11&rowBlue-1=0) | (colBlue+1=12&rowBlue-1=0) | (colBlue+1=13&rowBlue-1=0) | (colBlue+1=14&rowBlue-1=0) | (colBlue+1=0&rowBlue-1=1) | (colBlue+1=14&rowBlue-1=1) | (colBlue+1=0&rowBlue-1=2) | (colBlue+1=14&rowBlue-1=2) | (colBlue+1=0&rowBlue-1=3) | (colBlue+1=14&rowBlue-1=3) | (colBlue+1=0&rowBlue-1=4) | (colBlue+1=14&rowBlue-1=4) | (colBlue+1=0&rowBlue-1=5) | (colBlue+1=14&rowBlue-1=5) | (colBlue+1=0&rowBlue-1=6) | (colBlue+1=14&rowBlue-1=6) | (colBlue+1=0&rowBlue-1=7) | (colBlue+1=14&rowBlue-1=7) | (colBlue+1=0&rowBlue-1=8) | (colBlue+1=14&rowBlue-1=8) | (colBlue+1=0&rowBlue-1=9) | (colBlue+1=14&rowBlue-1=9) | (colBlue+1=0&rowBlue-1=10) | (colBlue+1=14&rowBlue-1=10) | (colBlue+1=0&rowBlue-1=11) | (colBlue+1=14&rowBlue-1=11) | (colBlue+1=0&rowBlue-1=12) | (colBlue+1=14&rowBlue-1=12) | (colBlue+1=0&rowBlue-1=13) | (colBlue+1=14&rowBlue-1=13) | (colBlue+1=0&rowBlue-1=14) | (colBlue+1=1&rowBlue-1=14) | (colBlue+1=2&rowBlue-1=14) | (colBlue+1=3&rowBlue-1=14) | (colBlue+1=4&rowBlue-1=14) | (colBlue+1=5&rowBlue-1=14) | (colBlue+1=6&rowBlue-1=14) | (colBlue+1=7&rowBlue-1=14) | (colBlue+1=8&rowBlue-1=14) | (colBlue+1=9&rowBlue-1=14) | (colBlue+1=10&rowBlue-1=14) | (colBlue+1=11&rowBlue-1=14) | (colBlue+1=12&rowBlue-1=14) | (colBlue+1=13&rowBlue-1=14) | (colBlue+1=14&rowBlue-1=14);
  42. formula BlueCannotSlipNorthWest = (colBlue-1=0&rowBlue-1=0) | (colBlue-1=1&rowBlue-1=0) | (colBlue-1=2&rowBlue-1=0) | (colBlue-1=3&rowBlue-1=0) | (colBlue-1=4&rowBlue-1=0) | (colBlue-1=5&rowBlue-1=0) | (colBlue-1=6&rowBlue-1=0) | (colBlue-1=7&rowBlue-1=0) | (colBlue-1=8&rowBlue-1=0) | (colBlue-1=9&rowBlue-1=0) | (colBlue-1=10&rowBlue-1=0) | (colBlue-1=11&rowBlue-1=0) | (colBlue-1=12&rowBlue-1=0) | (colBlue-1=13&rowBlue-1=0) | (colBlue-1=14&rowBlue-1=0) | (colBlue-1=0&rowBlue-1=1) | (colBlue-1=14&rowBlue-1=1) | (colBlue-1=0&rowBlue-1=2) | (colBlue-1=14&rowBlue-1=2) | (colBlue-1=0&rowBlue-1=3) | (colBlue-1=14&rowBlue-1=3) | (colBlue-1=0&rowBlue-1=4) | (colBlue-1=14&rowBlue-1=4) | (colBlue-1=0&rowBlue-1=5) | (colBlue-1=14&rowBlue-1=5) | (colBlue-1=0&rowBlue-1=6) | (colBlue-1=14&rowBlue-1=6) | (colBlue-1=0&rowBlue-1=7) | (colBlue-1=14&rowBlue-1=7) | (colBlue-1=0&rowBlue-1=8) | (colBlue-1=14&rowBlue-1=8) | (colBlue-1=0&rowBlue-1=9) | (colBlue-1=14&rowBlue-1=9) | (colBlue-1=0&rowBlue-1=10) | (colBlue-1=14&rowBlue-1=10) | (colBlue-1=0&rowBlue-1=11) | (colBlue-1=14&rowBlue-1=11) | (colBlue-1=0&rowBlue-1=12) | (colBlue-1=14&rowBlue-1=12) | (colBlue-1=0&rowBlue-1=13) | (colBlue-1=14&rowBlue-1=13) | (colBlue-1=0&rowBlue-1=14) | (colBlue-1=1&rowBlue-1=14) | (colBlue-1=2&rowBlue-1=14) | (colBlue-1=3&rowBlue-1=14) | (colBlue-1=4&rowBlue-1=14) | (colBlue-1=5&rowBlue-1=14) | (colBlue-1=6&rowBlue-1=14) | (colBlue-1=7&rowBlue-1=14) | (colBlue-1=8&rowBlue-1=14) | (colBlue-1=9&rowBlue-1=14) | (colBlue-1=10&rowBlue-1=14) | (colBlue-1=11&rowBlue-1=14) | (colBlue-1=12&rowBlue-1=14) | (colBlue-1=13&rowBlue-1=14) | (colBlue-1=14&rowBlue-1=14);
  43. formula BlueCannotSlipSouth = (colBlue=0&rowBlue+1=0) | (colBlue=1&rowBlue+1=0) | (colBlue=2&rowBlue+1=0) | (colBlue=3&rowBlue+1=0) | (colBlue=4&rowBlue+1=0) | (colBlue=5&rowBlue+1=0) | (colBlue=6&rowBlue+1=0) | (colBlue=7&rowBlue+1=0) | (colBlue=8&rowBlue+1=0) | (colBlue=9&rowBlue+1=0) | (colBlue=10&rowBlue+1=0) | (colBlue=11&rowBlue+1=0) | (colBlue=12&rowBlue+1=0) | (colBlue=13&rowBlue+1=0) | (colBlue=14&rowBlue+1=0) | (colBlue=0&rowBlue+1=1) | (colBlue=14&rowBlue+1=1) | (colBlue=0&rowBlue+1=2) | (colBlue=14&rowBlue+1=2) | (colBlue=0&rowBlue+1=3) | (colBlue=14&rowBlue+1=3) | (colBlue=0&rowBlue+1=4) | (colBlue=14&rowBlue+1=4) | (colBlue=0&rowBlue+1=5) | (colBlue=14&rowBlue+1=5) | (colBlue=0&rowBlue+1=6) | (colBlue=14&rowBlue+1=6) | (colBlue=0&rowBlue+1=7) | (colBlue=14&rowBlue+1=7) | (colBlue=0&rowBlue+1=8) | (colBlue=14&rowBlue+1=8) | (colBlue=0&rowBlue+1=9) | (colBlue=14&rowBlue+1=9) | (colBlue=0&rowBlue+1=10) | (colBlue=14&rowBlue+1=10) | (colBlue=0&rowBlue+1=11) | (colBlue=14&rowBlue+1=11) | (colBlue=0&rowBlue+1=12) | (colBlue=14&rowBlue+1=12) | (colBlue=0&rowBlue+1=13) | (colBlue=14&rowBlue+1=13) | (colBlue=0&rowBlue+1=14) | (colBlue=1&rowBlue+1=14) | (colBlue=2&rowBlue+1=14) | (colBlue=3&rowBlue+1=14) | (colBlue=4&rowBlue+1=14) | (colBlue=5&rowBlue+1=14) | (colBlue=6&rowBlue+1=14) | (colBlue=7&rowBlue+1=14) | (colBlue=8&rowBlue+1=14) | (colBlue=9&rowBlue+1=14) | (colBlue=10&rowBlue+1=14) | (colBlue=11&rowBlue+1=14) | (colBlue=12&rowBlue+1=14) | (colBlue=13&rowBlue+1=14) | (colBlue=14&rowBlue+1=14);
  44. formula BlueCannotSlipSouthEast = (colBlue+1=0&rowBlue+1=0) | (colBlue+1=1&rowBlue+1=0) | (colBlue+1=2&rowBlue+1=0) | (colBlue+1=3&rowBlue+1=0) | (colBlue+1=4&rowBlue+1=0) | (colBlue+1=5&rowBlue+1=0) | (colBlue+1=6&rowBlue+1=0) | (colBlue+1=7&rowBlue+1=0) | (colBlue+1=8&rowBlue+1=0) | (colBlue+1=9&rowBlue+1=0) | (colBlue+1=10&rowBlue+1=0) | (colBlue+1=11&rowBlue+1=0) | (colBlue+1=12&rowBlue+1=0) | (colBlue+1=13&rowBlue+1=0) | (colBlue+1=14&rowBlue+1=0) | (colBlue+1=0&rowBlue+1=1) | (colBlue+1=14&rowBlue+1=1) | (colBlue+1=0&rowBlue+1=2) | (colBlue+1=14&rowBlue+1=2) | (colBlue+1=0&rowBlue+1=3) | (colBlue+1=14&rowBlue+1=3) | (colBlue+1=0&rowBlue+1=4) | (colBlue+1=14&rowBlue+1=4) | (colBlue+1=0&rowBlue+1=5) | (colBlue+1=14&rowBlue+1=5) | (colBlue+1=0&rowBlue+1=6) | (colBlue+1=14&rowBlue+1=6) | (colBlue+1=0&rowBlue+1=7) | (colBlue+1=14&rowBlue+1=7) | (colBlue+1=0&rowBlue+1=8) | (colBlue+1=14&rowBlue+1=8) | (colBlue+1=0&rowBlue+1=9) | (colBlue+1=14&rowBlue+1=9) | (colBlue+1=0&rowBlue+1=10) | (colBlue+1=14&rowBlue+1=10) | (colBlue+1=0&rowBlue+1=11) | (colBlue+1=14&rowBlue+1=11) | (colBlue+1=0&rowBlue+1=12) | (colBlue+1=14&rowBlue+1=12) | (colBlue+1=0&rowBlue+1=13) | (colBlue+1=14&rowBlue+1=13) | (colBlue+1=0&rowBlue+1=14) | (colBlue+1=1&rowBlue+1=14) | (colBlue+1=2&rowBlue+1=14) | (colBlue+1=3&rowBlue+1=14) | (colBlue+1=4&rowBlue+1=14) | (colBlue+1=5&rowBlue+1=14) | (colBlue+1=6&rowBlue+1=14) | (colBlue+1=7&rowBlue+1=14) | (colBlue+1=8&rowBlue+1=14) | (colBlue+1=9&rowBlue+1=14) | (colBlue+1=10&rowBlue+1=14) | (colBlue+1=11&rowBlue+1=14) | (colBlue+1=12&rowBlue+1=14) | (colBlue+1=13&rowBlue+1=14) | (colBlue+1=14&rowBlue+1=14);
  45. formula BlueCannotSlipSouthWest = (colBlue-1=0&rowBlue+1=0) | (colBlue-1=1&rowBlue+1=0) | (colBlue-1=2&rowBlue+1=0) | (colBlue-1=3&rowBlue+1=0) | (colBlue-1=4&rowBlue+1=0) | (colBlue-1=5&rowBlue+1=0) | (colBlue-1=6&rowBlue+1=0) | (colBlue-1=7&rowBlue+1=0) | (colBlue-1=8&rowBlue+1=0) | (colBlue-1=9&rowBlue+1=0) | (colBlue-1=10&rowBlue+1=0) | (colBlue-1=11&rowBlue+1=0) | (colBlue-1=12&rowBlue+1=0) | (colBlue-1=13&rowBlue+1=0) | (colBlue-1=14&rowBlue+1=0) | (colBlue-1=0&rowBlue+1=1) | (colBlue-1=14&rowBlue+1=1) | (colBlue-1=0&rowBlue+1=2) | (colBlue-1=14&rowBlue+1=2) | (colBlue-1=0&rowBlue+1=3) | (colBlue-1=14&rowBlue+1=3) | (colBlue-1=0&rowBlue+1=4) | (colBlue-1=14&rowBlue+1=4) | (colBlue-1=0&rowBlue+1=5) | (colBlue-1=14&rowBlue+1=5) | (colBlue-1=0&rowBlue+1=6) | (colBlue-1=14&rowBlue+1=6) | (colBlue-1=0&rowBlue+1=7) | (colBlue-1=14&rowBlue+1=7) | (colBlue-1=0&rowBlue+1=8) | (colBlue-1=14&rowBlue+1=8) | (colBlue-1=0&rowBlue+1=9) | (colBlue-1=14&rowBlue+1=9) | (colBlue-1=0&rowBlue+1=10) | (colBlue-1=14&rowBlue+1=10) | (colBlue-1=0&rowBlue+1=11) | (colBlue-1=14&rowBlue+1=11) | (colBlue-1=0&rowBlue+1=12) | (colBlue-1=14&rowBlue+1=12) | (colBlue-1=0&rowBlue+1=13) | (colBlue-1=14&rowBlue+1=13) | (colBlue-1=0&rowBlue+1=14) | (colBlue-1=1&rowBlue+1=14) | (colBlue-1=2&rowBlue+1=14) | (colBlue-1=3&rowBlue+1=14) | (colBlue-1=4&rowBlue+1=14) | (colBlue-1=5&rowBlue+1=14) | (colBlue-1=6&rowBlue+1=14) | (colBlue-1=7&rowBlue+1=14) | (colBlue-1=8&rowBlue+1=14) | (colBlue-1=9&rowBlue+1=14) | (colBlue-1=10&rowBlue+1=14) | (colBlue-1=11&rowBlue+1=14) | (colBlue-1=12&rowBlue+1=14) | (colBlue-1=13&rowBlue+1=14) | (colBlue-1=14&rowBlue+1=14);
  46. formula BlueCannotSlipWest = (colBlue-1=0&rowBlue=0) | (colBlue-1=1&rowBlue=0) | (colBlue-1=2&rowBlue=0) | (colBlue-1=3&rowBlue=0) | (colBlue-1=4&rowBlue=0) | (colBlue-1=5&rowBlue=0) | (colBlue-1=6&rowBlue=0) | (colBlue-1=7&rowBlue=0) | (colBlue-1=8&rowBlue=0) | (colBlue-1=9&rowBlue=0) | (colBlue-1=10&rowBlue=0) | (colBlue-1=11&rowBlue=0) | (colBlue-1=12&rowBlue=0) | (colBlue-1=13&rowBlue=0) | (colBlue-1=14&rowBlue=0) | (colBlue-1=0&rowBlue=1) | (colBlue-1=14&rowBlue=1) | (colBlue-1=0&rowBlue=2) | (colBlue-1=14&rowBlue=2) | (colBlue-1=0&rowBlue=3) | (colBlue-1=14&rowBlue=3) | (colBlue-1=0&rowBlue=4) | (colBlue-1=14&rowBlue=4) | (colBlue-1=0&rowBlue=5) | (colBlue-1=14&rowBlue=5) | (colBlue-1=0&rowBlue=6) | (colBlue-1=14&rowBlue=6) | (colBlue-1=0&rowBlue=7) | (colBlue-1=14&rowBlue=7) | (colBlue-1=0&rowBlue=8) | (colBlue-1=14&rowBlue=8) | (colBlue-1=0&rowBlue=9) | (colBlue-1=14&rowBlue=9) | (colBlue-1=0&rowBlue=10) | (colBlue-1=14&rowBlue=10) | (colBlue-1=0&rowBlue=11) | (colBlue-1=14&rowBlue=11) | (colBlue-1=0&rowBlue=12) | (colBlue-1=14&rowBlue=12) | (colBlue-1=0&rowBlue=13) | (colBlue-1=14&rowBlue=13) | (colBlue-1=0&rowBlue=14) | (colBlue-1=1&rowBlue=14) | (colBlue-1=2&rowBlue=14) | (colBlue-1=3&rowBlue=14) | (colBlue-1=4&rowBlue=14) | (colBlue-1=5&rowBlue=14) | (colBlue-1=6&rowBlue=14) | (colBlue-1=7&rowBlue=14) | (colBlue-1=8&rowBlue=14) | (colBlue-1=9&rowBlue=14) | (colBlue-1=10&rowBlue=14) | (colBlue-1=11&rowBlue=14) | (colBlue-1=12&rowBlue=14) | (colBlue-1=13&rowBlue=14) | (colBlue-1=14&rowBlue=14);
  47. formula BlueIsOnLava = (colBlue=7&rowBlue=1) | (colBlue=8&rowBlue=1) | (colBlue=9&rowBlue=1) | (colBlue=10&rowBlue=1) | (colBlue=7&rowBlue=2) | (colBlue=8&rowBlue=2) | (colBlue=9&rowBlue=2) | (colBlue=10&rowBlue=2) | (colBlue=4&rowBlue=5) | (colBlue=5&rowBlue=5) | (colBlue=11&rowBlue=7) | (colBlue=12&rowBlue=7) | (colBlue=13&rowBlue=7) | (colBlue=11&rowBlue=8) | (colBlue=12&rowBlue=8) | (colBlue=13&rowBlue=8) | (colBlue=4&rowBlue=9) | (colBlue=5&rowBlue=9) | (colBlue=11&rowBlue=9) | (colBlue=12&rowBlue=9) | (colBlue=13&rowBlue=9) | (colBlue=4&rowBlue=10) | (colBlue=5&rowBlue=10) | (colBlue=4&rowBlue=11) | (colBlue=5&rowBlue=11);
  48. formula BlueIsOnGoal = (colBlue=13&rowBlue=1);
  49. formula collision = (colAgent=colBlue&rowAgent=rowBlue);
  50. label "collision" = collision;
  51. init
  52. true
  53. endinit
  56. module Agent
  57. colAgent : [1..13];
  58. rowAgent : [1..13];
  59. viewAgent : [0..3];
  61. [Agent_turn_right] !AgentIsOnSlippery & !AgentIsOnLava &true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  62. [Agent_turn_left] !AgentIsOnSlippery & !AgentIsOnLava &viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  63. [Agent_turn_left] !AgentIsOnSlippery & !AgentIsOnLava &viewAgent=0 -> 1.000000: (viewAgent'=3);
  64. [Agent_move_North] viewAgent=3 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
  65. [Agent_move_East] viewAgent=0 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveEastWall -> 1.000000: (colAgent'=colAgent+1);
  66. [Agent_move_South] viewAgent=1 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1);
  67. [Agent_move_West] viewAgent=2 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1);
  68. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.025000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.025000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  69. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & !AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 0.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  70. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  71. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  72. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  73. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1);
  74. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & !AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  75. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> true;
  76. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & !AgentCannotSlipWest & !AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  77. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & AgentCannotSlipWest & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  78. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & !AgentCannotSlipWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1);
  79. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & AgentCannotSlipWest & AgentCannotSlipNorthWest -> true;
  80. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & !AgentCannotSlipEast & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  81. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & AgentCannotSlipEast & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  82. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & !AgentCannotSlipEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1);
  83. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & AgentCannotSlipEast & AgentCannotSlipNorthEast -> true;
  84. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorth & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: true;
  85. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorth & AgentCannotSlipSouth -> 1.000000: true;
  86. [Agent_turn_right] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (rowAgent'=rowAgent-1);
  87. [Agent_turn_right] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  88. [Agent_turn_left] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (rowAgent'=rowAgent-1);
  89. [Agent_turn_left] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (rowAgent'=rowAgent-1);
  90. [Agent_turn_left] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  91. [Agent_turn_left] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & viewAgent=0 -> 1.000000: (viewAgent'=3);
  92. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.025000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1) + 0.025000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  93. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 0.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1) + 0.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  94. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  95. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  96. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  97. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1);
  98. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  99. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> true;
  100. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  101. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  102. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1);
  103. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> true;
  104. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & !AgentCannotSlipSouth & !AgentCannotSlipSouthEast -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  105. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & AgentCannotSlipSouth & !AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  106. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & !AgentCannotSlipSouth & AgentCannotSlipSouthEast -> 1.000000: (rowAgent'=rowAgent+1);
  107. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & AgentCannotSlipSouth & AgentCannotSlipSouthEast -> true;
  108. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyEast & !AgentCannotSlipEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: true;
  109. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyEast & AgentCannotSlipEast -> 1.000000: true;
  110. [Agent_turn_right] AgentIsOnSlipperyEast & !AgentCannotSlipEast & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (colAgent'=colAgent+1);
  111. [Agent_turn_right] AgentIsOnSlipperyEast & AgentCannotSlipEast & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  112. [Agent_turn_left] AgentIsOnSlipperyEast & !AgentCannotSlipEast & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (colAgent'=colAgent+1);
  113. [Agent_turn_left] AgentIsOnSlipperyEast & !AgentCannotSlipEast & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (colAgent'=colAgent+1);
  114. [Agent_turn_left] AgentIsOnSlipperyEast & AgentCannotSlipEast & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  115. [Agent_turn_left] AgentIsOnSlipperyEast & AgentCannotSlipEast & viewAgent=0 -> 1.000000: (viewAgent'=3);
  116. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & !AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.025000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1) + 0.025000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  117. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & !AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 0.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1) + 0.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  118. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  119. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & !AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  120. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  121. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1);
  122. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & !AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  123. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> true;
  124. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & !AgentCannotSlipWest & !AgentCannotSlipSouthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  125. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & AgentCannotSlipWest & !AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  126. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & !AgentCannotSlipWest & AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1);
  127. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & AgentCannotSlipWest & AgentCannotSlipSouthWest -> true;
  128. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & !AgentCannotSlipEast & !AgentCannotSlipSouthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  129. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & AgentCannotSlipEast & !AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  130. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & !AgentCannotSlipEast & AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1);
  131. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & AgentCannotSlipEast & AgentCannotSlipSouthEast -> true;
  132. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: true;
  133. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperySouth & AgentCannotSlipSouth -> 1.000000: true;
  134. [Agent_turn_right] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (rowAgent'=rowAgent+1);
  135. [Agent_turn_right] AgentIsOnSlipperySouth & AgentCannotSlipSouth & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  136. [Agent_turn_left] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (rowAgent'=rowAgent+1);
  137. [Agent_turn_left] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (rowAgent'=rowAgent+1);
  138. [Agent_turn_left] AgentIsOnSlipperySouth & AgentCannotSlipSouth & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  139. [Agent_turn_left] AgentIsOnSlipperySouth & AgentCannotSlipSouth & viewAgent=0 -> 1.000000: (viewAgent'=3);
  140. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & !AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.025000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1) + 0.025000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  141. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & !AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 0.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1) + 0.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  142. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  143. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & !AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  144. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  145. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1);
  146. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & !AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  147. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> true;
  148. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  149. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & AgentCannotSlipNorth & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  150. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & !AgentCannotSlipNorth & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1);
  151. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & AgentCannotSlipNorth & AgentCannotSlipNorthWest -> true;
  152. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & !AgentCannotSlipSouth & !AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  153. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & AgentCannotSlipSouth & !AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  154. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & !AgentCannotSlipSouth & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1);
  155. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & AgentCannotSlipSouth & AgentCannotSlipSouthWest -> true;
  156. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyWest & !AgentCannotSlipWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: true;
  157. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyWest & AgentCannotSlipWest -> 1.000000: true;
  158. [Agent_turn_right] AgentIsOnSlipperyWest & !AgentCannotSlipWest & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (colAgent'=colAgent-1);
  159. [Agent_turn_right] AgentIsOnSlipperyWest & AgentCannotSlipWest & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  160. [Agent_turn_left] AgentIsOnSlipperyWest & !AgentCannotSlipWest & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (colAgent'=colAgent-1);
  161. [Agent_turn_left] AgentIsOnSlipperyWest & !AgentCannotSlipWest & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (colAgent'=colAgent-1);
  162. [Agent_turn_left] AgentIsOnSlipperyWest & AgentCannotSlipWest & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  163. [Agent_turn_left] AgentIsOnSlipperyWest & AgentCannotSlipWest & viewAgent=0 -> 1.000000: (viewAgent'=3);
  164. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  165. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  166. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast -> 1.000000: (colAgent'=colAgent+1);
  167. [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast -> 1.000000: true;
  168. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipNorth -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  169. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipNorth -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  170. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipNorth -> 1.000000: (rowAgent'=rowAgent-1);
  171. [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipNorth -> 1.000000: true;
  172. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent+1) + 0.016667: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.016667: (colAgent'=colAgent+1) + 0.016667: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  173. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.333333: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.333333: (colAgent'=colAgent+1) + 0.333333: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  174. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.050847: (colAgent'=colAgent+1);
  175. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.500000: (colAgent'=colAgent+1);
  176. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.050847: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  177. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.500000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  178. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent+1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  179. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  180. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.050847: (colAgent'=colAgent+1) + 0.050847: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  181. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.500000: (colAgent'=colAgent+1) + 0.500000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  182. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.051724: (colAgent'=colAgent+1);
  183. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (colAgent'=colAgent+1);
  184. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.051724: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  185. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  186. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent+1);
  187. [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: true;
  188. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & !AgentCannotSlipNorthWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent-1) + 0.016667: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.016667: (rowAgent'=rowAgent-1) + 0.016667: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  189. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & !AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.966102: (colAgent'=colAgent-1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.050847: (rowAgent'=rowAgent-1);
  190. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.966102: (colAgent'=colAgent-1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  191. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  192. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.966102: (colAgent'=colAgent-1) + 0.050847: (rowAgent'=rowAgent-1) + 0.050847: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  193. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1);
  194. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  195. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent-1);
  196. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.333333: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.333333: (rowAgent'=rowAgent-1) + 0.333333: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  197. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.500000: (rowAgent'=rowAgent-1);
  198. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  199. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  200. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.500000: (rowAgent'=rowAgent-1) + 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  201. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1);
  202. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  203. [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: true;
  204. [Agent_turn_right] AgentIsOnSlipperyNorthEast & true & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  205. [Agent_turn_left] AgentIsOnSlipperyNorthEast & true & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  206. [Agent_turn_left] AgentIsOnSlipperyNorthEast & true & viewAgent=0 -> 1.000000: (viewAgent'=3);
  207. [Agent_on_goal]AgentIsOnGoal & clock=0 -> true;
  208. endmodule
  211. module Blue
  212. colBlue : [1..13];
  213. rowBlue : [1..13];
  214. viewBlue : [0..3];
  216. [Blue_turn_right] !BlueIsOnSlippery & !BlueIsOnLava &true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  217. [Blue_turn_left] !BlueIsOnSlippery & !BlueIsOnLava &viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  218. [Blue_turn_left] !BlueIsOnSlippery & !BlueIsOnLava &viewBlue=0 -> 1.000000: (viewBlue'=3);
  219. [Blue_move_North] viewBlue=3 & !BlueIsOnSlippery & !BlueIsOnLava & !BlueIsOnGoal & !BlueCannotMoveNorthWall -> 1.000000: (rowBlue'=rowBlue-1);
  220. [Blue_move_East] viewBlue=0 & !BlueIsOnSlippery & !BlueIsOnLava & !BlueIsOnGoal & !BlueCannotMoveEastWall -> 1.000000: (colBlue'=colBlue+1);
  221. [Blue_move_South] viewBlue=1 & !BlueIsOnSlippery & !BlueIsOnLava & !BlueIsOnGoal & !BlueCannotMoveSouthWall -> 1.000000: (rowBlue'=rowBlue+1);
  222. [Blue_move_West] viewBlue=2 & !BlueIsOnSlippery & !BlueIsOnLava & !BlueIsOnGoal & !BlueCannotMoveWestWall -> 1.000000: (colBlue'=colBlue-1);
  223. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast & !BlueCannotSlipNorthWest -> 0.950000: (rowBlue'=rowBlue-1) + 0.025000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.025000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  224. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & BlueCannotSlipNorth & !BlueCannotSlipNorthEast & !BlueCannotSlipNorthWest -> 0.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  225. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & BlueCannotSlipNorthEast & !BlueCannotSlipNorthWest -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  226. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast & BlueCannotSlipNorthWest -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  227. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & BlueCannotSlipNorth & BlueCannotSlipNorthEast & !BlueCannotSlipNorthWest -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  228. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & BlueCannotSlipNorthEast & BlueCannotSlipNorthWest -> 1.000000: (rowBlue'=rowBlue-1);
  229. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & BlueCannotSlipNorth & !BlueCannotSlipNorthEast & BlueCannotSlipNorthWest -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  230. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorth & BlueCannotSlipNorth & BlueCannotSlipNorthEast & BlueCannotSlipNorthWest -> true;
  231. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorth & !BlueCannotSlipWest & !BlueCannotSlipNorthWest -> 0.950000: (colBlue'=colBlue-1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  232. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorth & BlueCannotSlipWest & !BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  233. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorth & !BlueCannotSlipWest & BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1);
  234. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorth & BlueCannotSlipWest & BlueCannotSlipNorthWest -> true;
  235. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorth & !BlueCannotSlipEast & !BlueCannotSlipNorthEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  236. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorth & BlueCannotSlipEast & !BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  237. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorth & !BlueCannotSlipEast & BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1);
  238. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorth & BlueCannotSlipEast & BlueCannotSlipNorthEast -> true;
  239. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorth & !BlueCannotSlipSouth -> 0.950000: (rowBlue'=rowBlue+1) + 0.050000: true;
  240. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorth & BlueCannotSlipSouth -> 1.000000: true;
  241. [Blue_turn_right] BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & true -> 0.950000: (viewBlue'=mod(viewBlue+1,4)) + 0.050000: (rowBlue'=rowBlue-1);
  242. [Blue_turn_right] BlueIsOnSlipperyNorth & BlueCannotSlipNorth & true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  243. [Blue_turn_left] BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & viewBlue>0 -> 0.950000: (viewBlue'=viewBlue-1) + 0.050000: (rowBlue'=rowBlue-1);
  244. [Blue_turn_left] BlueIsOnSlipperyNorth & !BlueCannotSlipNorth & viewBlue=0 -> 0.950000: (viewBlue'=3) + 0.050000: (rowBlue'=rowBlue-1);
  245. [Blue_turn_left] BlueIsOnSlipperyNorth & BlueCannotSlipNorth & viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  246. [Blue_turn_left] BlueIsOnSlipperyNorth & BlueCannotSlipNorth & viewBlue=0 -> 1.000000: (viewBlue'=3);
  247. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipNorthEast -> 0.950000: (colBlue'=colBlue+1) + 0.025000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1) + 0.025000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  248. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipNorthEast -> 0.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1) + 0.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  249. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipNorthEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  250. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipNorthEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  251. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  252. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1);
  253. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  254. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipNorthEast -> true;
  255. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyEast & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  256. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyEast & BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  257. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyEast & !BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 1.000000: (rowBlue'=rowBlue-1);
  258. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyEast & BlueCannotSlipNorth & BlueCannotSlipNorthEast -> true;
  259. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyEast & !BlueCannotSlipSouth & !BlueCannotSlipSouthEast -> 0.950000: (rowBlue'=rowBlue+1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  260. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyEast & BlueCannotSlipSouth & !BlueCannotSlipSouthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  261. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyEast & !BlueCannotSlipSouth & BlueCannotSlipSouthEast -> 1.000000: (rowBlue'=rowBlue+1);
  262. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyEast & BlueCannotSlipSouth & BlueCannotSlipSouthEast -> true;
  263. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyEast & !BlueCannotSlipEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: true;
  264. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyEast & BlueCannotSlipEast -> 1.000000: true;
  265. [Blue_turn_right] BlueIsOnSlipperyEast & !BlueCannotSlipEast & true -> 0.950000: (viewBlue'=mod(viewBlue+1,4)) + 0.050000: (colBlue'=colBlue+1);
  266. [Blue_turn_right] BlueIsOnSlipperyEast & BlueCannotSlipEast & true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  267. [Blue_turn_left] BlueIsOnSlipperyEast & !BlueCannotSlipEast & viewBlue>0 -> 0.950000: (viewBlue'=viewBlue-1) + 0.050000: (colBlue'=colBlue+1);
  268. [Blue_turn_left] BlueIsOnSlipperyEast & !BlueCannotSlipEast & viewBlue=0 -> 0.950000: (viewBlue'=3) + 0.050000: (colBlue'=colBlue+1);
  269. [Blue_turn_left] BlueIsOnSlipperyEast & BlueCannotSlipEast & viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  270. [Blue_turn_left] BlueIsOnSlipperyEast & BlueCannotSlipEast & viewBlue=0 -> 1.000000: (viewBlue'=3);
  271. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & !BlueCannotSlipSouth & !BlueCannotSlipSouthEast & !BlueCannotSlipSouthWest -> 0.950000: (rowBlue'=rowBlue+1) + 0.025000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1) + 0.025000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue-1);
  272. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & BlueCannotSlipSouth & !BlueCannotSlipSouthEast & !BlueCannotSlipSouthWest -> 0.000000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1) + 0.000000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue-1);
  273. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & !BlueCannotSlipSouth & BlueCannotSlipSouthEast & !BlueCannotSlipSouthWest -> 0.950000: (rowBlue'=rowBlue+1) + 0.050000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue-1);
  274. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & !BlueCannotSlipSouth & !BlueCannotSlipSouthEast & BlueCannotSlipSouthWest -> 0.950000: (rowBlue'=rowBlue+1) + 0.050000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  275. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & BlueCannotSlipSouth & BlueCannotSlipSouthEast & !BlueCannotSlipSouthWest -> 1.000000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue-1);
  276. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & !BlueCannotSlipSouth & BlueCannotSlipSouthEast & BlueCannotSlipSouthWest -> 1.000000: (rowBlue'=rowBlue+1);
  277. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & BlueCannotSlipSouth & !BlueCannotSlipSouthEast & BlueCannotSlipSouthWest -> 1.000000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  278. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperySouth & BlueCannotSlipSouth & BlueCannotSlipSouthEast & BlueCannotSlipSouthWest -> true;
  279. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperySouth & !BlueCannotSlipWest & !BlueCannotSlipSouthWest -> 0.950000: (colBlue'=colBlue-1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  280. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperySouth & BlueCannotSlipWest & !BlueCannotSlipSouthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  281. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperySouth & !BlueCannotSlipWest & BlueCannotSlipSouthWest -> 1.000000: (colBlue'=colBlue-1);
  282. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperySouth & BlueCannotSlipWest & BlueCannotSlipSouthWest -> true;
  283. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperySouth & !BlueCannotSlipEast & !BlueCannotSlipSouthEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  284. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperySouth & BlueCannotSlipEast & !BlueCannotSlipSouthEast -> 1.000000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue+1);
  285. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperySouth & !BlueCannotSlipEast & BlueCannotSlipSouthEast -> 1.000000: (colBlue'=colBlue+1);
  286. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperySouth & BlueCannotSlipEast & BlueCannotSlipSouthEast -> true;
  287. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperySouth & !BlueCannotSlipSouth -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: true;
  288. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperySouth & BlueCannotSlipSouth -> 1.000000: true;
  289. [Blue_turn_right] BlueIsOnSlipperySouth & !BlueCannotSlipSouth & true -> 0.950000: (viewBlue'=mod(viewBlue+1,4)) + 0.050000: (rowBlue'=rowBlue+1);
  290. [Blue_turn_right] BlueIsOnSlipperySouth & BlueCannotSlipSouth & true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  291. [Blue_turn_left] BlueIsOnSlipperySouth & !BlueCannotSlipSouth & viewBlue>0 -> 0.950000: (viewBlue'=viewBlue-1) + 0.050000: (rowBlue'=rowBlue+1);
  292. [Blue_turn_left] BlueIsOnSlipperySouth & !BlueCannotSlipSouth & viewBlue=0 -> 0.950000: (viewBlue'=3) + 0.050000: (rowBlue'=rowBlue+1);
  293. [Blue_turn_left] BlueIsOnSlipperySouth & BlueCannotSlipSouth & viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  294. [Blue_turn_left] BlueIsOnSlipperySouth & BlueCannotSlipSouth & viewBlue=0 -> 1.000000: (viewBlue'=3);
  295. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & !BlueCannotSlipWest & !BlueCannotSlipSouthWest & !BlueCannotSlipNorthWest -> 0.950000: (colBlue'=colBlue-1) + 0.025000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1) + 0.025000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  296. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & BlueCannotSlipWest & !BlueCannotSlipSouthWest & !BlueCannotSlipNorthWest -> 0.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1) + 0.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  297. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & !BlueCannotSlipWest & BlueCannotSlipSouthWest & !BlueCannotSlipNorthWest -> 0.950000: (colBlue'=colBlue-1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  298. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & !BlueCannotSlipWest & !BlueCannotSlipSouthWest & BlueCannotSlipNorthWest -> 0.950000: (colBlue'=colBlue-1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  299. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & BlueCannotSlipWest & BlueCannotSlipSouthWest & !BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  300. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & !BlueCannotSlipWest & BlueCannotSlipSouthWest & BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1);
  301. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & BlueCannotSlipWest & !BlueCannotSlipSouthWest & BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  302. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyWest & BlueCannotSlipWest & BlueCannotSlipSouthWest & BlueCannotSlipNorthWest -> true;
  303. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyWest & !BlueCannotSlipNorth & !BlueCannotSlipNorthWest -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  304. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyWest & BlueCannotSlipNorth & !BlueCannotSlipNorthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue-1);
  305. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyWest & !BlueCannotSlipNorth & BlueCannotSlipNorthWest -> 1.000000: (rowBlue'=rowBlue-1);
  306. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyWest & BlueCannotSlipNorth & BlueCannotSlipNorthWest -> true;
  307. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyWest & !BlueCannotSlipSouth & !BlueCannotSlipSouthWest -> 0.950000: (rowBlue'=rowBlue+1) + 0.050000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  308. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyWest & BlueCannotSlipSouth & !BlueCannotSlipSouthWest -> 1.000000: (colBlue'=colBlue-1)&(rowBlue'=rowBlue+1);
  309. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyWest & !BlueCannotSlipSouth & BlueCannotSlipSouthWest -> 1.000000: (rowBlue'=rowBlue+1);
  310. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyWest & BlueCannotSlipSouth & BlueCannotSlipSouthWest -> true;
  311. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyWest & !BlueCannotSlipWest -> 0.950000: (colBlue'=colBlue-1) + 0.050000: true;
  312. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyWest & BlueCannotSlipWest -> 1.000000: true;
  313. [Blue_turn_right] BlueIsOnSlipperyWest & !BlueCannotSlipWest & true -> 0.950000: (viewBlue'=mod(viewBlue+1,4)) + 0.050000: (colBlue'=colBlue-1);
  314. [Blue_turn_right] BlueIsOnSlipperyWest & BlueCannotSlipWest & true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  315. [Blue_turn_left] BlueIsOnSlipperyWest & !BlueCannotSlipWest & viewBlue>0 -> 0.950000: (viewBlue'=viewBlue-1) + 0.050000: (colBlue'=colBlue-1);
  316. [Blue_turn_left] BlueIsOnSlipperyWest & !BlueCannotSlipWest & viewBlue=0 -> 0.950000: (viewBlue'=3) + 0.050000: (colBlue'=colBlue-1);
  317. [Blue_turn_left] BlueIsOnSlipperyWest & BlueCannotSlipWest & viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  318. [Blue_turn_left] BlueIsOnSlipperyWest & BlueCannotSlipWest & viewBlue=0 -> 1.000000: (viewBlue'=3);
  319. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipEast -> 0.950000: (colBlue'=colBlue+1) + 0.050000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  320. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipEast -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  321. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipEast -> 1.000000: (colBlue'=colBlue+1);
  322. [Blue_move_East] viewBlue=0 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipEast -> 1.000000: true;
  323. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipNorth -> 0.950000: (rowBlue'=rowBlue-1) + 0.050000: (colBlue'=colBlue+1)&(rowBlue'=rowBlue-1);
  324. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipNorth -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  325. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipNorth -> 1.000000: (rowBlue'=rowBlue-1);
  326. [Blue_move_North] viewBlue=3 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipNorth -> 1.000000: true;
  327. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.950000: (rowBlue'=rowBlue+1) + 0.016667: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.016667: (colBlue'=colBlue+1) + 0.016667: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  328. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 0.333333: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.333333: (colBlue'=colBlue+1) + 0.333333: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  329. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.982759: (rowBlue'=rowBlue+1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.050847: (colBlue'=colBlue+1);
  330. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.500000: (colBlue'=colBlue+1);
  331. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.982759: (rowBlue'=rowBlue+1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.050847: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  332. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1) + 0.500000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  333. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.950000: (rowBlue'=rowBlue+1) + 0.051724: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  334. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipNorthEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  335. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.982759: (rowBlue'=rowBlue+1) + 0.050847: (colBlue'=colBlue+1) + 0.050847: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  336. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 0.500000: (colBlue'=colBlue+1) + 0.500000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  337. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.982759: (rowBlue'=rowBlue+1) + 0.051724: (colBlue'=colBlue+1);
  338. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & !BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 1.000000: (colBlue'=colBlue+1);
  339. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 0.982759: (rowBlue'=rowBlue+1) + 0.051724: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  340. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipEast & !BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 1.000000: (rowBlue'=rowBlue+1)&(colBlue'=colBlue+1);
  341. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & !BlueCannotSlipSouth -> 1.000000: (rowBlue'=rowBlue+1);
  342. [Blue_move_South] viewBlue=1 & BlueIsOnSlipperyNorthEast & BlueCannotSlipNorthEast & BlueCannotSlipEast & BlueCannotSlipSouthEast & BlueCannotSlipSouth -> 1.000000: true;
  343. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & !BlueCannotSlipNorthWest & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.950000: (colBlue'=colBlue-1) + 0.016667: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.016667: (rowBlue'=rowBlue-1) + 0.016667: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  344. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & !BlueCannotSlipNorthWest & !BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 0.966102: (colBlue'=colBlue-1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.050847: (rowBlue'=rowBlue-1);
  345. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & !BlueCannotSlipNorthWest & BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.966102: (colBlue'=colBlue-1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  346. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & !BlueCannotSlipNorthWest & BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 0.982759: (colBlue'=colBlue-1) + 0.051724: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  347. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & BlueCannotSlipNorthWest & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.966102: (colBlue'=colBlue-1) + 0.050847: (rowBlue'=rowBlue-1) + 0.050847: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  348. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & BlueCannotSlipNorthWest & !BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 0.982759: (colBlue'=colBlue-1) + 0.051724: (rowBlue'=rowBlue-1);
  349. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & BlueCannotSlipNorthWest & BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.982759: (colBlue'=colBlue-1) + 0.051724: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  350. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & !BlueCannotSlipWest & BlueCannotSlipNorthWest & BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 1.000000: (colBlue'=colBlue-1);
  351. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & !BlueCannotSlipNorthWest & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.333333: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.333333: (rowBlue'=rowBlue-1) + 0.333333: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  352. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & !BlueCannotSlipNorthWest & !BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.500000: (rowBlue'=rowBlue-1);
  353. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & !BlueCannotSlipNorthWest & BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1) + 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  354. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & !BlueCannotSlipNorthWest & BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue-1);
  355. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & BlueCannotSlipNorthWest & !BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 0.500000: (rowBlue'=rowBlue-1) + 0.500000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  356. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & BlueCannotSlipNorthWest & !BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 1.000000: (rowBlue'=rowBlue-1);
  357. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & BlueCannotSlipNorthWest & BlueCannotSlipNorth & !BlueCannotSlipNorthEast -> 1.000000: (rowBlue'=rowBlue-1)&(colBlue'=colBlue+1);
  358. [Blue_move_West] viewBlue=2 & BlueIsOnSlipperyNorthEast & BlueCannotSlipWest & BlueCannotSlipNorthWest & BlueCannotSlipNorth & BlueCannotSlipNorthEast -> 1.000000: true;
  359. [Blue_turn_right] BlueIsOnSlipperyNorthEast & true & true -> 1.000000: (viewBlue'=mod(viewBlue+1,4));
  360. [Blue_turn_left] BlueIsOnSlipperyNorthEast & true & viewBlue>0 -> 1.000000: (viewBlue'=viewBlue-1);
  361. [Blue_turn_left] BlueIsOnSlipperyNorthEast & true & viewBlue=0 -> 1.000000: (viewBlue'=3);
  362. endmodule
  365. module Arbiter
  366. clock : [0..1];
  367. [Agent_turn_left] clock=0 -> (clock'=1) ;
  368. [Agent_turn_right] clock=0 -> (clock'=1) ;
  369. [Agent_move_East] clock=0 -> (clock'=1) ;
  370. [Agent_move_North] clock=0 -> (clock'=1) ;
  371. [Agent_move_South] clock=0 -> (clock'=1) ;
  372. [Agent_move_West] clock=0 -> (clock'=1) ;
  373. [Blue_turn_left] clock=1 -> (clock'=0) ;
  374. [Blue_turn_right] clock=1 -> (clock'=0) ;
  375. [Blue_move_East] clock=1 -> (clock'=0) ;
  376. [Blue_move_North] clock=1 -> (clock'=0) ;
  377. [Blue_move_South] clock=1 -> (clock'=0) ;
  378. [Blue_move_West] clock=1 -> (clock'=0) ;
  379. endmodule
  381. player Agent
  382. [Agent_turn_left], [Agent_turn_right], [Agent_move_East], [Agent_move_North], [Agent_move_South], [Agent_move_West], [Agent_on_goal]
  383. endplayer
  384. player Blue
  385. [Blue_turn_left], [Blue_turn_right], [Blue_move_East], [Blue_move_North], [Blue_move_South], [Blue_move_West]
  386. endplayer