mdp

formula AgentCannotMoveEastWall = (colAgent=25&rowAgent=10) | (colAgent=25&rowAgent=14) | (colAgent=25&rowAgent=15) | (colAgent=25&rowAgent=16) | (colAgent=25&rowAgent=17);
formula AgentCannotMoveNorthWall = (colAgent=16&rowAgent=1) | (colAgent=17&rowAgent=1) | (colAgent=18&rowAgent=1) | (colAgent=19&rowAgent=1);
formula AgentCannotMoveSouthWall = false;
formula AgentCannotMoveWestWall = (colAgent=1&rowAgent=4);
formula AgentIsOnSlipperyEast = (colAgent=10&rowAgent=2) | (colAgent=11&rowAgent=2) | (colAgent=12&rowAgent=2) | (colAgent=16&rowAgent=3) | (colAgent=17&rowAgent=3) | (colAgent=18&rowAgent=3) | (colAgent=19&rowAgent=3) | (colAgent=16&rowAgent=6) | (colAgent=17&rowAgent=6) | (colAgent=18&rowAgent=6) | (colAgent=19&rowAgent=6) | (colAgent=20&rowAgent=6) | (colAgent=21&rowAgent=6) | (colAgent=22&rowAgent=6) | (colAgent=1&rowAgent=7) | (colAgent=2&rowAgent=7) | (colAgent=3&rowAgent=7) | (colAgent=4&rowAgent=7) | (colAgent=5&rowAgent=7) | (colAgent=6&rowAgent=7) | (colAgent=7&rowAgent=7) | (colAgent=8&rowAgent=7) | (colAgent=9&rowAgent=7) | (colAgent=10&rowAgent=7) | (colAgent=11&rowAgent=7) | (colAgent=1&rowAgent=8) | (colAgent=2&rowAgent=8) | (colAgent=3&rowAgent=8) | (colAgent=4&rowAgent=8) | (colAgent=5&rowAgent=8) | (colAgent=6&rowAgent=8) | (colAgent=7&rowAgent=8) | (colAgent=8&rowAgent=8) | (colAgent=1&rowAgent=9) | (colAgent=2&rowAgent=9) | (colAgent=3&rowAgent=9) | (colAgent=4&rowAgent=9) | (colAgent=5&rowAgent=9) | (colAgent=6&rowAgent=9) | (colAgent=7&rowAgent=9) | (colAgent=8&rowAgent=9) | (colAgent=1&rowAgent=10) | (colAgent=2&rowAgent=10) | (colAgent=3&rowAgent=10) | (colAgent=4&rowAgent=10) | (colAgent=5&rowAgent=10) | (colAgent=6&rowAgent=10) | (colAgent=7&rowAgent=10) | (colAgent=16&rowAgent=12) | (colAgent=17&rowAgent=12) | (colAgent=18&rowAgent=12) | (colAgent=19&rowAgent=12) | (colAgent=20&rowAgent=12) | (colAgent=21&rowAgent=12) | (colAgent=22&rowAgent=13) | (colAgent=23&rowAgent=13) | (colAgent=24&rowAgent=13) | (colAgent=25&rowAgent=13) | (colAgent=1&rowAgent=17) | (colAgent=2&rowAgent=17) | (colAgent=3&rowAgent=17) | (colAgent=4&rowAgent=17) | (colAgent=5&rowAgent=17) | (colAgent=6&rowAgent=17) | (colAgent=7&rowAgent=17) | (colAgent=8&rowAgent=17) | (colAgent=9&rowAgent=17) | (colAgent=10&rowAgent=17) | (colAgent=11&rowAgent=17) | (colAgent=12&rowAgent=17) | (colAgent=13&rowAgent=17) | (colAgent=14&rowAgent=17) | (colAgent=15&rowAgent=17) | (colAgent=1&rowAgent=18) | (colAgent=2&rowAgent=18) | (colAgent=3&rowAgent=18) | (colAgent=4&rowAgent=18) | (colAgent=5&rowAgent=18) | (colAgent=6&rowAgent=18) | (colAgent=7&rowAgent=18) | (colAgent=8&rowAgent=18) | (colAgent=9&rowAgent=18) | (colAgent=10&rowAgent=18) | (colAgent=11&rowAgent=18) | (colAgent=12&rowAgent=18) | (colAgent=13&rowAgent=18) | (colAgent=14&rowAgent=18) | (colAgent=15&rowAgent=18) | (colAgent=16&rowAgent=18) | (colAgent=22&rowAgent=18) | (colAgent=23&rowAgent=18) | (colAgent=24&rowAgent=18) | (colAgent=25&rowAgent=18) | (colAgent=1&rowAgent=19) | (colAgent=2&rowAgent=19) | (colAgent=3&rowAgent=19) | (colAgent=4&rowAgent=19) | (colAgent=5&rowAgent=19) | (colAgent=6&rowAgent=19) | (colAgent=7&rowAgent=19) | (colAgent=8&rowAgent=19) | (colAgent=9&rowAgent=19) | (colAgent=10&rowAgent=19) | (colAgent=11&rowAgent=19) | (colAgent=12&rowAgent=19) | (colAgent=13&rowAgent=19) | (colAgent=14&rowAgent=19) | (colAgent=15&rowAgent=19) | (colAgent=16&rowAgent=19) | (colAgent=17&rowAgent=19) | (colAgent=1&rowAgent=20) | (colAgent=2&rowAgent=20) | (colAgent=3&rowAgent=20) | (colAgent=4&rowAgent=20) | (colAgent=5&rowAgent=20) | (colAgent=6&rowAgent=20) | (colAgent=7&rowAgent=20) | (colAgent=8&rowAgent=20) | (colAgent=9&rowAgent=20) | (colAgent=10&rowAgent=20) | (colAgent=11&rowAgent=20) | (colAgent=12&rowAgent=20) | (colAgent=13&rowAgent=20) | (colAgent=14&rowAgent=20) | (colAgent=15&rowAgent=20) | (colAgent=16&rowAgent=20) | (colAgent=17&rowAgent=20) | (colAgent=18&rowAgent=20);
formula AgentIsOnSlipperyNorth = (colAgent=15&rowAgent=1) | (colAgent=20&rowAgent=1) | (colAgent=15&rowAgent=2) | (colAgent=20&rowAgent=2) | (colAgent=13&rowAgent=3) | (colAgent=13&rowAgent=4) | (colAgent=13&rowAgent=5) | (colAgent=13&rowAgent=6) | (colAgent=15&rowAgent=7) | (colAgent=24&rowAgent=7) | (colAgent=15&rowAgent=8) | (colAgent=24&rowAgent=8) | (colAgent=15&rowAgent=9) | (colAgent=24&rowAgent=9) | (colAgent=15&rowAgent=10) | (colAgent=24&rowAgent=10) | (colAgent=13&rowAgent=11) | (colAgent=15&rowAgent=11) | (colAgent=24&rowAgent=11) | (colAgent=13&rowAgent=12) | (colAgent=13&rowAgent=13) | (colAgent=13&rowAgent=14) | (colAgent=21&rowAgent=14) | (colAgent=13&rowAgent=15) | (colAgent=21&rowAgent=15) | (colAgent=13&rowAgent=16) | (colAgent=21&rowAgent=16) | (colAgent=21&rowAgent=17);
formula AgentIsOnSlipperyNorthEast = (colAgent=1&rowAgent=1) | (colAgent=2&rowAgent=1) | (colAgent=3&rowAgent=1) | (colAgent=4&rowAgent=1) | (colAgent=5&rowAgent=1) | (colAgent=6&rowAgent=1) | (colAgent=7&rowAgent=1) | (colAgent=8&rowAgent=1) | (colAgent=9&rowAgent=1) | (colAgent=10&rowAgent=1) | (colAgent=11&rowAgent=1) | (colAgent=12&rowAgent=1) | (colAgent=13&rowAgent=1) | (colAgent=14&rowAgent=1) | (colAgent=21&rowAgent=1) | (colAgent=22&rowAgent=1) | (colAgent=23&rowAgent=1) | (colAgent=24&rowAgent=1) | (colAgent=25&rowAgent=1) | (colAgent=1&rowAgent=2) | (colAgent=2&rowAgent=2) | (colAgent=3&rowAgent=2) | (colAgent=4&rowAgent=2) | (colAgent=5&rowAgent=2) | (colAgent=6&rowAgent=2) | (colAgent=7&rowAgent=2) | (colAgent=8&rowAgent=2) | (colAgent=9&rowAgent=2) | (colAgent=13&rowAgent=2) | (colAgent=14&rowAgent=2) | (colAgent=21&rowAgent=2) | (colAgent=22&rowAgent=2) | (colAgent=23&rowAgent=2) | (colAgent=24&rowAgent=2) | (colAgent=25&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=7&rowAgent=3) | (colAgent=8&rowAgent=3) | (colAgent=9&rowAgent=3) | (colAgent=14&rowAgent=3) | (colAgent=15&rowAgent=3) | (colAgent=20&rowAgent=3) | (colAgent=21&rowAgent=3) | (colAgent=22&rowAgent=3) | (colAgent=23&rowAgent=3) | (colAgent=24&rowAgent=3) | (colAgent=25&rowAgent=3) | (colAgent=1&rowAgent=4) | (colAgent=2&rowAgent=4) | (colAgent=3&rowAgent=4) | (colAgent=4&rowAgent=4) | (colAgent=5&rowAgent=4) | (colAgent=6&rowAgent=4) | (colAgent=7&rowAgent=4) | (colAgent=8&rowAgent=4) | (colAgent=9&rowAgent=4) | (colAgent=14&rowAgent=4) | (colAgent=15&rowAgent=4) | (colAgent=16&rowAgent=4) | (colAgent=17&rowAgent=4) | (colAgent=18&rowAgent=4) | (colAgent=19&rowAgent=4) | (colAgent=20&rowAgent=4) | (colAgent=21&rowAgent=4) | (colAgent=22&rowAgent=4) | (colAgent=23&rowAgent=4) | (colAgent=24&rowAgent=4) | (colAgent=25&rowAgent=4) | (colAgent=1&rowAgent=5) | (colAgent=2&rowAgent=5) | (colAgent=3&rowAgent=5) | (colAgent=4&rowAgent=5) | (colAgent=5&rowAgent=5) | (colAgent=6&rowAgent=5) | (colAgent=7&rowAgent=5) | (colAgent=8&rowAgent=5) | (colAgent=9&rowAgent=5) | (colAgent=14&rowAgent=5) | (colAgent=15&rowAgent=5) | (colAgent=16&rowAgent=5) | (colAgent=17&rowAgent=5) | (colAgent=18&rowAgent=5) | (colAgent=19&rowAgent=5) | (colAgent=20&rowAgent=5) | (colAgent=21&rowAgent=5) | (colAgent=22&rowAgent=5) | (colAgent=23&rowAgent=5) | (colAgent=24&rowAgent=5) | (colAgent=25&rowAgent=5) | (colAgent=1&rowAgent=6) | (colAgent=2&rowAgent=6) | (colAgent=3&rowAgent=6) | (colAgent=4&rowAgent=6) | (colAgent=5&rowAgent=6) | (colAgent=6&rowAgent=6) | (colAgent=7&rowAgent=6) | (colAgent=8&rowAgent=6) | (colAgent=9&rowAgent=6) | (colAgent=14&rowAgent=6) | (colAgent=15&rowAgent=6) | (colAgent=23&rowAgent=6) | (colAgent=24&rowAgent=6) | (colAgent=25&rowAgent=6) | (colAgent=13&rowAgent=7) | (colAgent=14&rowAgent=7) | (colAgent=25&rowAgent=7) | (colAgent=9&rowAgent=8) | (colAgent=10&rowAgent=8) | (colAgent=11&rowAgent=8) | (colAgent=13&rowAgent=8) | (colAgent=14&rowAgent=8) | (colAgent=25&rowAgent=8) | (colAgent=9&rowAgent=9) | (colAgent=13&rowAgent=9) | (colAgent=14&rowAgent=9) | (colAgent=25&rowAgent=9) | (colAgent=8&rowAgent=10) | (colAgent=13&rowAgent=10) | (colAgent=14&rowAgent=10) | (colAgent=1&rowAgent=11) | (colAgent=2&rowAgent=11) | (colAgent=3&rowAgent=11) | (colAgent=4&rowAgent=11) | (colAgent=5&rowAgent=11) | (colAgent=6&rowAgent=11) | (colAgent=7&rowAgent=11) | (colAgent=14&rowAgent=11) | (colAgent=25&rowAgent=11) | (colAgent=1&rowAgent=12) | (colAgent=2&rowAgent=12) | (colAgent=3&rowAgent=12) | (colAgent=4&rowAgent=12) | (colAgent=5&rowAgent=12) | (colAgent=6&rowAgent=12) | (colAgent=7&rowAgent=12) | (colAgent=14&rowAgent=12) | (colAgent=15&rowAgent=12) | (colAgent=22&rowAgent=12) | (colAgent=23&rowAgent=12) | (colAgent=24&rowAgent=12) | (colAgent=25&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=14&rowAgent=13) | (colAgent=15&rowAgent=13) | (colAgent=16&rowAgent=13) | (colAgent=17&rowAgent=13) | (colAgent=18&rowAgent=13) | (colAgent=19&rowAgent=13) | (colAgent=20&rowAgent=13) | (colAgent=21&rowAgent=13) | (colAgent=1&rowAgent=14) | (colAgent=2&rowAgent=14) | (colAgent=3&rowAgent=14) | (colAgent=4&rowAgent=14) | (colAgent=5&rowAgent=14) | (colAgent=6&rowAgent=14) | (colAgent=7&rowAgent=14) | (colAgent=14&rowAgent=14) | (colAgent=15&rowAgent=14) | (colAgent=16&rowAgent=14) | (colAgent=17&rowAgent=14) | (colAgent=18&rowAgent=14) | (colAgent=19&rowAgent=14) | (colAgent=20&rowAgent=14) | (colAgent=1&rowAgent=15) | (colAgent=2&rowAgent=15) | (colAgent=3&rowAgent=15) | (colAgent=4&rowAgent=15) | (colAgent=5&rowAgent=15) | (colAgent=6&rowAgent=15) | (colAgent=7&rowAgent=15) | (colAgent=14&rowAgent=15) | (colAgent=15&rowAgent=15) | (colAgent=16&rowAgent=15) | (colAgent=17&rowAgent=15) | (colAgent=18&rowAgent=15) | (colAgent=19&rowAgent=15) | (colAgent=20&rowAgent=15) | (colAgent=1&rowAgent=16) | (colAgent=2&rowAgent=16) | (colAgent=3&rowAgent=16) | (colAgent=4&rowAgent=16) | (colAgent=5&rowAgent=16) | (colAgent=6&rowAgent=16) | (colAgent=7&rowAgent=16) | (colAgent=14&rowAgent=16) | (colAgent=15&rowAgent=16) | (colAgent=16&rowAgent=16) | (colAgent=17&rowAgent=16) | (colAgent=18&rowAgent=16) | (colAgent=19&rowAgent=16) | (colAgent=20&rowAgent=16) | (colAgent=16&rowAgent=17) | (colAgent=17&rowAgent=17) | (colAgent=18&rowAgent=17) | (colAgent=19&rowAgent=17) | (colAgent=20&rowAgent=17) | (colAgent=17&rowAgent=18) | (colAgent=18&rowAgent=18) | (colAgent=19&rowAgent=18) | (colAgent=20&rowAgent=18) | (colAgent=21&rowAgent=18) | (colAgent=18&rowAgent=19) | (colAgent=19&rowAgent=19) | (colAgent=20&rowAgent=19) | (colAgent=21&rowAgent=19) | (colAgent=22&rowAgent=19) | (colAgent=23&rowAgent=19) | (colAgent=24&rowAgent=19) | (colAgent=25&rowAgent=19) | (colAgent=19&rowAgent=20) | (colAgent=20&rowAgent=20) | (colAgent=21&rowAgent=20) | (colAgent=22&rowAgent=20) | (colAgent=23&rowAgent=20) | (colAgent=24&rowAgent=20) | (colAgent=25&rowAgent=20);
formula AgentIsOnSlipperyNorthWest = false;
formula AgentIsOnSlipperySouth = (colAgent=12&rowAgent=7) | (colAgent=12&rowAgent=8) | (colAgent=12&rowAgent=9) | (colAgent=12&rowAgent=10);
formula AgentIsOnSlipperySouthEast = false;
formula AgentIsOnSlipperySouthWest = false;
formula AgentIsOnSlipperyWest = (colAgent=10&rowAgent=9) | (colAgent=11&rowAgent=9) | (colAgent=9&rowAgent=10) | (colAgent=10&rowAgent=10) | (colAgent=11&rowAgent=10);
formula AgentIsOnSlippery = AgentIsOnSlipperyEast | AgentIsOnSlipperyNorth | AgentIsOnSlipperyNorthEast | AgentIsOnSlipperyNorthWest | AgentIsOnSlipperySouth | AgentIsOnSlipperySouthEast | AgentIsOnSlipperySouthWest | AgentIsOnSlipperyWest;
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=15&rowAgent=0) | (colAgent+1=16&rowAgent=0) | (colAgent+1=17&rowAgent=0) | (colAgent+1=18&rowAgent=0) | (colAgent+1=19&rowAgent=0) | (colAgent+1=20&rowAgent=0) | (colAgent+1=21&rowAgent=0) | (colAgent+1=22&rowAgent=0) | (colAgent+1=23&rowAgent=0) | (colAgent+1=24&rowAgent=0) | (colAgent+1=25&rowAgent=0) | (colAgent+1=26&rowAgent=0) | (colAgent+1=0&rowAgent=1) | (colAgent+1=26&rowAgent=1) | (colAgent+1=0&rowAgent=2) | (colAgent+1=26&rowAgent=2) | (colAgent+1=0&rowAgent=3) | (colAgent+1=26&rowAgent=3) | (colAgent+1=0&rowAgent=4) | (colAgent+1=26&rowAgent=4) | (colAgent+1=0&rowAgent=5) | (colAgent+1=26&rowAgent=5) | (colAgent+1=0&rowAgent=6) | (colAgent+1=26&rowAgent=6) | (colAgent+1=0&rowAgent=7) | (colAgent+1=26&rowAgent=7) | (colAgent+1=0&rowAgent=8) | (colAgent+1=26&rowAgent=8) | (colAgent+1=0&rowAgent=9) | (colAgent+1=26&rowAgent=9) | (colAgent+1=0&rowAgent=10) | (colAgent+1=26&rowAgent=10) | (colAgent+1=0&rowAgent=11) | (colAgent+1=26&rowAgent=11) | (colAgent+1=0&rowAgent=12) | (colAgent+1=26&rowAgent=12) | (colAgent+1=0&rowAgent=13) | (colAgent+1=26&rowAgent=13) | (colAgent+1=0&rowAgent=14) | (colAgent+1=26&rowAgent=14) | (colAgent+1=0&rowAgent=15) | (colAgent+1=26&rowAgent=15) | (colAgent+1=0&rowAgent=16) | (colAgent+1=26&rowAgent=16) | (colAgent+1=0&rowAgent=17) | (colAgent+1=26&rowAgent=17) | (colAgent+1=0&rowAgent=18) | (colAgent+1=26&rowAgent=18) | (colAgent+1=0&rowAgent=19) | (colAgent+1=26&rowAgent=19) | (colAgent+1=0&rowAgent=20) | (colAgent+1=26&rowAgent=20) | (colAgent+1=0&rowAgent=21) | (colAgent+1=1&rowAgent=21) | (colAgent+1=2&rowAgent=21) | (colAgent+1=3&rowAgent=21) | (colAgent+1=4&rowAgent=21) | (colAgent+1=5&rowAgent=21) | (colAgent+1=6&rowAgent=21) | (colAgent+1=7&rowAgent=21) | (colAgent+1=8&rowAgent=21) | (colAgent+1=9&rowAgent=21) | (colAgent+1=10&rowAgent=21) | (colAgent+1=11&rowAgent=21) | (colAgent+1=12&rowAgent=21) | (colAgent+1=13&rowAgent=21) | (colAgent+1=14&rowAgent=21) | (colAgent+1=15&rowAgent=21) | (colAgent+1=16&rowAgent=21) | (colAgent+1=17&rowAgent=21) | (colAgent+1=18&rowAgent=21) | (colAgent+1=19&rowAgent=21) | (colAgent+1=20&rowAgent=21) | (colAgent+1=21&rowAgent=21) | (colAgent+1=22&rowAgent=21) | (colAgent+1=23&rowAgent=21) | (colAgent+1=24&rowAgent=21) | (colAgent+1=25&rowAgent=21) | (colAgent+1=26&rowAgent=21);
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=15&rowAgent-1=0) | (colAgent=16&rowAgent-1=0) | (colAgent=17&rowAgent-1=0) | (colAgent=18&rowAgent-1=0) | (colAgent=19&rowAgent-1=0) | (colAgent=20&rowAgent-1=0) | (colAgent=21&rowAgent-1=0) | (colAgent=22&rowAgent-1=0) | (colAgent=23&rowAgent-1=0) | (colAgent=24&rowAgent-1=0) | (colAgent=25&rowAgent-1=0) | (colAgent=26&rowAgent-1=0) | (colAgent=0&rowAgent-1=1) | (colAgent=26&rowAgent-1=1) | (colAgent=0&rowAgent-1=2) | (colAgent=26&rowAgent-1=2) | (colAgent=0&rowAgent-1=3) | (colAgent=26&rowAgent-1=3) | (colAgent=0&rowAgent-1=4) | (colAgent=26&rowAgent-1=4) | (colAgent=0&rowAgent-1=5) | (colAgent=26&rowAgent-1=5) | (colAgent=0&rowAgent-1=6) | (colAgent=26&rowAgent-1=6) | (colAgent=0&rowAgent-1=7) | (colAgent=26&rowAgent-1=7) | (colAgent=0&rowAgent-1=8) | (colAgent=26&rowAgent-1=8) | (colAgent=0&rowAgent-1=9) | (colAgent=26&rowAgent-1=9) | (colAgent=0&rowAgent-1=10) | (colAgent=26&rowAgent-1=10) | (colAgent=0&rowAgent-1=11) | (colAgent=26&rowAgent-1=11) | (colAgent=0&rowAgent-1=12) | (colAgent=26&rowAgent-1=12) | (colAgent=0&rowAgent-1=13) | (colAgent=26&rowAgent-1=13) | (colAgent=0&rowAgent-1=14) | (colAgent=26&rowAgent-1=14) | (colAgent=0&rowAgent-1=15) | (colAgent=26&rowAgent-1=15) | (colAgent=0&rowAgent-1=16) | (colAgent=26&rowAgent-1=16) | (colAgent=0&rowAgent-1=17) | (colAgent=26&rowAgent-1=17) | (colAgent=0&rowAgent-1=18) | (colAgent=26&rowAgent-1=18) | (colAgent=0&rowAgent-1=19) | (colAgent=26&rowAgent-1=19) | (colAgent=0&rowAgent-1=20) | (colAgent=26&rowAgent-1=20) | (colAgent=0&rowAgent-1=21) | (colAgent=1&rowAgent-1=21) | (colAgent=2&rowAgent-1=21) | (colAgent=3&rowAgent-1=21) | (colAgent=4&rowAgent-1=21) | (colAgent=5&rowAgent-1=21) | (colAgent=6&rowAgent-1=21) | (colAgent=7&rowAgent-1=21) | (colAgent=8&rowAgent-1=21) | (colAgent=9&rowAgent-1=21) | (colAgent=10&rowAgent-1=21) | (colAgent=11&rowAgent-1=21) | (colAgent=12&rowAgent-1=21) | (colAgent=13&rowAgent-1=21) | (colAgent=14&rowAgent-1=21) | (colAgent=15&rowAgent-1=21) | (colAgent=16&rowAgent-1=21) | (colAgent=17&rowAgent-1=21) | (colAgent=18&rowAgent-1=21) | (colAgent=19&rowAgent-1=21) | (colAgent=20&rowAgent-1=21) | (colAgent=21&rowAgent-1=21) | (colAgent=22&rowAgent-1=21) | (colAgent=23&rowAgent-1=21) | (colAgent=24&rowAgent-1=21) | (colAgent=25&rowAgent-1=21) | (colAgent=26&rowAgent-1=21);
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=15&rowAgent-1=0) | (colAgent+1=16&rowAgent-1=0) | (colAgent+1=17&rowAgent-1=0) | (colAgent+1=18&rowAgent-1=0) | (colAgent+1=19&rowAgent-1=0) | (colAgent+1=20&rowAgent-1=0) | (colAgent+1=21&rowAgent-1=0) | (colAgent+1=22&rowAgent-1=0) | (colAgent+1=23&rowAgent-1=0) | (colAgent+1=24&rowAgent-1=0) | (colAgent+1=25&rowAgent-1=0) | (colAgent+1=26&rowAgent-1=0) | (colAgent+1=0&rowAgent-1=1) | (colAgent+1=26&rowAgent-1=1) | (colAgent+1=0&rowAgent-1=2) | (colAgent+1=26&rowAgent-1=2) | (colAgent+1=0&rowAgent-1=3) | (colAgent+1=26&rowAgent-1=3) | (colAgent+1=0&rowAgent-1=4) | (colAgent+1=26&rowAgent-1=4) | (colAgent+1=0&rowAgent-1=5) | (colAgent+1=26&rowAgent-1=5) | (colAgent+1=0&rowAgent-1=6) | (colAgent+1=26&rowAgent-1=6) | (colAgent+1=0&rowAgent-1=7) | (colAgent+1=26&rowAgent-1=7) | (colAgent+1=0&rowAgent-1=8) | (colAgent+1=26&rowAgent-1=8) | (colAgent+1=0&rowAgent-1=9) | (colAgent+1=26&rowAgent-1=9) | (colAgent+1=0&rowAgent-1=10) | (colAgent+1=26&rowAgent-1=10) | (colAgent+1=0&rowAgent-1=11) | (colAgent+1=26&rowAgent-1=11) | (colAgent+1=0&rowAgent-1=12) | (colAgent+1=26&rowAgent-1=12) | (colAgent+1=0&rowAgent-1=13) | (colAgent+1=26&rowAgent-1=13) | (colAgent+1=0&rowAgent-1=14) | (colAgent+1=26&rowAgent-1=14) | (colAgent+1=0&rowAgent-1=15) | (colAgent+1=26&rowAgent-1=15) | (colAgent+1=0&rowAgent-1=16) | (colAgent+1=26&rowAgent-1=16) | (colAgent+1=0&rowAgent-1=17) | (colAgent+1=26&rowAgent-1=17) | (colAgent+1=0&rowAgent-1=18) | (colAgent+1=26&rowAgent-1=18) | (colAgent+1=0&rowAgent-1=19) | (colAgent+1=26&rowAgent-1=19) | (colAgent+1=0&rowAgent-1=20) | (colAgent+1=26&rowAgent-1=20) | (colAgent+1=0&rowAgent-1=21) | (colAgent+1=1&rowAgent-1=21) | (colAgent+1=2&rowAgent-1=21) | (colAgent+1=3&rowAgent-1=21) | (colAgent+1=4&rowAgent-1=21) | (colAgent+1=5&rowAgent-1=21) | (colAgent+1=6&rowAgent-1=21) | (colAgent+1=7&rowAgent-1=21) | (colAgent+1=8&rowAgent-1=21) | (colAgent+1=9&rowAgent-1=21) | (colAgent+1=10&rowAgent-1=21) | (colAgent+1=11&rowAgent-1=21) | (colAgent+1=12&rowAgent-1=21) | (colAgent+1=13&rowAgent-1=21) | (colAgent+1=14&rowAgent-1=21) | (colAgent+1=15&rowAgent-1=21) | (colAgent+1=16&rowAgent-1=21) | (colAgent+1=17&rowAgent-1=21) | (colAgent+1=18&rowAgent-1=21) | (colAgent+1=19&rowAgent-1=21) | (colAgent+1=20&rowAgent-1=21) | (colAgent+1=21&rowAgent-1=21) | (colAgent+1=22&rowAgent-1=21) | (colAgent+1=23&rowAgent-1=21) | (colAgent+1=24&rowAgent-1=21) | (colAgent+1=25&rowAgent-1=21) | (colAgent+1=26&rowAgent-1=21);
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=15&rowAgent-1=0) | (colAgent-1=16&rowAgent-1=0) | (colAgent-1=17&rowAgent-1=0) | (colAgent-1=18&rowAgent-1=0) | (colAgent-1=19&rowAgent-1=0) | (colAgent-1=20&rowAgent-1=0) | (colAgent-1=21&rowAgent-1=0) | (colAgent-1=22&rowAgent-1=0) | (colAgent-1=23&rowAgent-1=0) | (colAgent-1=24&rowAgent-1=0) | (colAgent-1=25&rowAgent-1=0) | (colAgent-1=26&rowAgent-1=0) | (colAgent-1=0&rowAgent-1=1) | (colAgent-1=26&rowAgent-1=1) | (colAgent-1=0&rowAgent-1=2) | (colAgent-1=26&rowAgent-1=2) | (colAgent-1=0&rowAgent-1=3) | (colAgent-1=26&rowAgent-1=3) | (colAgent-1=0&rowAgent-1=4) | (colAgent-1=26&rowAgent-1=4) | (colAgent-1=0&rowAgent-1=5) | (colAgent-1=26&rowAgent-1=5) | (colAgent-1=0&rowAgent-1=6) | (colAgent-1=26&rowAgent-1=6) | (colAgent-1=0&rowAgent-1=7) | (colAgent-1=26&rowAgent-1=7) | (colAgent-1=0&rowAgent-1=8) | (colAgent-1=26&rowAgent-1=8) | (colAgent-1=0&rowAgent-1=9) | (colAgent-1=26&rowAgent-1=9) | (colAgent-1=0&rowAgent-1=10) | (colAgent-1=26&rowAgent-1=10) | (colAgent-1=0&rowAgent-1=11) | (colAgent-1=26&rowAgent-1=11) | (colAgent-1=0&rowAgent-1=12) | (colAgent-1=26&rowAgent-1=12) | (colAgent-1=0&rowAgent-1=13) | (colAgent-1=26&rowAgent-1=13) | (colAgent-1=0&rowAgent-1=14) | (colAgent-1=26&rowAgent-1=14) | (colAgent-1=0&rowAgent-1=15) | (colAgent-1=26&rowAgent-1=15) | (colAgent-1=0&rowAgent-1=16) | (colAgent-1=26&rowAgent-1=16) | (colAgent-1=0&rowAgent-1=17) | (colAgent-1=26&rowAgent-1=17) | (colAgent-1=0&rowAgent-1=18) | (colAgent-1=26&rowAgent-1=18) | (colAgent-1=0&rowAgent-1=19) | (colAgent-1=26&rowAgent-1=19) | (colAgent-1=0&rowAgent-1=20) | (colAgent-1=26&rowAgent-1=20) | (colAgent-1=0&rowAgent-1=21) | (colAgent-1=1&rowAgent-1=21) | (colAgent-1=2&rowAgent-1=21) | (colAgent-1=3&rowAgent-1=21) | (colAgent-1=4&rowAgent-1=21) | (colAgent-1=5&rowAgent-1=21) | (colAgent-1=6&rowAgent-1=21) | (colAgent-1=7&rowAgent-1=21) | (colAgent-1=8&rowAgent-1=21) | (colAgent-1=9&rowAgent-1=21) | (colAgent-1=10&rowAgent-1=21) | (colAgent-1=11&rowAgent-1=21) | (colAgent-1=12&rowAgent-1=21) | (colAgent-1=13&rowAgent-1=21) | (colAgent-1=14&rowAgent-1=21) | (colAgent-1=15&rowAgent-1=21) | (colAgent-1=16&rowAgent-1=21) | (colAgent-1=17&rowAgent-1=21) | (colAgent-1=18&rowAgent-1=21) | (colAgent-1=19&rowAgent-1=21) | (colAgent-1=20&rowAgent-1=21) | (colAgent-1=21&rowAgent-1=21) | (colAgent-1=22&rowAgent-1=21) | (colAgent-1=23&rowAgent-1=21) | (colAgent-1=24&rowAgent-1=21) | (colAgent-1=25&rowAgent-1=21) | (colAgent-1=26&rowAgent-1=21);
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=15&rowAgent+1=0) | (colAgent=16&rowAgent+1=0) | (colAgent=17&rowAgent+1=0) | (colAgent=18&rowAgent+1=0) | (colAgent=19&rowAgent+1=0) | (colAgent=20&rowAgent+1=0) | (colAgent=21&rowAgent+1=0) | (colAgent=22&rowAgent+1=0) | (colAgent=23&rowAgent+1=0) | (colAgent=24&rowAgent+1=0) | (colAgent=25&rowAgent+1=0) | (colAgent=26&rowAgent+1=0) | (colAgent=0&rowAgent+1=1) | (colAgent=26&rowAgent+1=1) | (colAgent=0&rowAgent+1=2) | (colAgent=26&rowAgent+1=2) | (colAgent=0&rowAgent+1=3) | (colAgent=26&rowAgent+1=3) | (colAgent=0&rowAgent+1=4) | (colAgent=26&rowAgent+1=4) | (colAgent=0&rowAgent+1=5) | (colAgent=26&rowAgent+1=5) | (colAgent=0&rowAgent+1=6) | (colAgent=26&rowAgent+1=6) | (colAgent=0&rowAgent+1=7) | (colAgent=26&rowAgent+1=7) | (colAgent=0&rowAgent+1=8) | (colAgent=26&rowAgent+1=8) | (colAgent=0&rowAgent+1=9) | (colAgent=26&rowAgent+1=9) | (colAgent=0&rowAgent+1=10) | (colAgent=26&rowAgent+1=10) | (colAgent=0&rowAgent+1=11) | (colAgent=26&rowAgent+1=11) | (colAgent=0&rowAgent+1=12) | (colAgent=26&rowAgent+1=12) | (colAgent=0&rowAgent+1=13) | (colAgent=26&rowAgent+1=13) | (colAgent=0&rowAgent+1=14) | (colAgent=26&rowAgent+1=14) | (colAgent=0&rowAgent+1=15) | (colAgent=26&rowAgent+1=15) | (colAgent=0&rowAgent+1=16) | (colAgent=26&rowAgent+1=16) | (colAgent=0&rowAgent+1=17) | (colAgent=26&rowAgent+1=17) | (colAgent=0&rowAgent+1=18) | (colAgent=26&rowAgent+1=18) | (colAgent=0&rowAgent+1=19) | (colAgent=26&rowAgent+1=19) | (colAgent=0&rowAgent+1=20) | (colAgent=26&rowAgent+1=20) | (colAgent=0&rowAgent+1=21) | (colAgent=1&rowAgent+1=21) | (colAgent=2&rowAgent+1=21) | (colAgent=3&rowAgent+1=21) | (colAgent=4&rowAgent+1=21) | (colAgent=5&rowAgent+1=21) | (colAgent=6&rowAgent+1=21) | (colAgent=7&rowAgent+1=21) | (colAgent=8&rowAgent+1=21) | (colAgent=9&rowAgent+1=21) | (colAgent=10&rowAgent+1=21) | (colAgent=11&rowAgent+1=21) | (colAgent=12&rowAgent+1=21) | (colAgent=13&rowAgent+1=21) | (colAgent=14&rowAgent+1=21) | (colAgent=15&rowAgent+1=21) | (colAgent=16&rowAgent+1=21) | (colAgent=17&rowAgent+1=21) | (colAgent=18&rowAgent+1=21) | (colAgent=19&rowAgent+1=21) | (colAgent=20&rowAgent+1=21) | (colAgent=21&rowAgent+1=21) | (colAgent=22&rowAgent+1=21) | (colAgent=23&rowAgent+1=21) | (colAgent=24&rowAgent+1=21) | (colAgent=25&rowAgent+1=21) | (colAgent=26&rowAgent+1=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=15&rowAgent+1=0) | (colAgent+1=16&rowAgent+1=0) | (colAgent+1=17&rowAgent+1=0) | (colAgent+1=18&rowAgent+1=0) | (colAgent+1=19&rowAgent+1=0) | (colAgent+1=20&rowAgent+1=0) | (colAgent+1=21&rowAgent+1=0) | (colAgent+1=22&rowAgent+1=0) | (colAgent+1=23&rowAgent+1=0) | (colAgent+1=24&rowAgent+1=0) | (colAgent+1=25&rowAgent+1=0) | (colAgent+1=26&rowAgent+1=0) | (colAgent+1=0&rowAgent+1=1) | (colAgent+1=26&rowAgent+1=1) | (colAgent+1=0&rowAgent+1=2) | (colAgent+1=26&rowAgent+1=2) | (colAgent+1=0&rowAgent+1=3) | (colAgent+1=26&rowAgent+1=3) | (colAgent+1=0&rowAgent+1=4) | (colAgent+1=26&rowAgent+1=4) | (colAgent+1=0&rowAgent+1=5) | (colAgent+1=26&rowAgent+1=5) | (colAgent+1=0&rowAgent+1=6) | (colAgent+1=26&rowAgent+1=6) | (colAgent+1=0&rowAgent+1=7) | (colAgent+1=26&rowAgent+1=7) | (colAgent+1=0&rowAgent+1=8) | (colAgent+1=26&rowAgent+1=8) | (colAgent+1=0&rowAgent+1=9) | (colAgent+1=26&rowAgent+1=9) | (colAgent+1=0&rowAgent+1=10) | (colAgent+1=26&rowAgent+1=10) | (colAgent+1=0&rowAgent+1=11) | (colAgent+1=26&rowAgent+1=11) | (colAgent+1=0&rowAgent+1=12) | (colAgent+1=26&rowAgent+1=12) | (colAgent+1=0&rowAgent+1=13) | (colAgent+1=26&rowAgent+1=13) | (colAgent+1=0&rowAgent+1=14) | (colAgent+1=26&rowAgent+1=14) | (colAgent+1=0&rowAgent+1=15) | (colAgent+1=26&rowAgent+1=15) | (colAgent+1=0&rowAgent+1=16) | (colAgent+1=26&rowAgent+1=16) | (colAgent+1=0&rowAgent+1=17) | (colAgent+1=26&rowAgent+1=17) | (colAgent+1=0&rowAgent+1=18) | (colAgent+1=26&rowAgent+1=18) | (colAgent+1=0&rowAgent+1=19) | (colAgent+1=26&rowAgent+1=19) | (colAgent+1=0&rowAgent+1=20) | (colAgent+1=26&rowAgent+1=20) | (colAgent+1=0&rowAgent+1=21) | (colAgent+1=1&rowAgent+1=21) | (colAgent+1=2&rowAgent+1=21) | (colAgent+1=3&rowAgent+1=21) | (colAgent+1=4&rowAgent+1=21) | (colAgent+1=5&rowAgent+1=21) | (colAgent+1=6&rowAgent+1=21) | (colAgent+1=7&rowAgent+1=21) | (colAgent+1=8&rowAgent+1=21) | (colAgent+1=9&rowAgent+1=21) | (colAgent+1=10&rowAgent+1=21) | (colAgent+1=11&rowAgent+1=21) | (colAgent+1=12&rowAgent+1=21) | (colAgent+1=13&rowAgent+1=21) | (colAgent+1=14&rowAgent+1=21) | (colAgent+1=15&rowAgent+1=21) | (colAgent+1=16&rowAgent+1=21) | (colAgent+1=17&rowAgent+1=21) | (colAgent+1=18&rowAgent+1=21) | (colAgent+1=19&rowAgent+1=21) | (colAgent+1=20&rowAgent+1=21) | (colAgent+1=21&rowAgent+1=21) | (colAgent+1=22&rowAgent+1=21) | (colAgent+1=23&rowAgent+1=21) | (colAgent+1=24&rowAgent+1=21) | (colAgent+1=25&rowAgent+1=21) | (colAgent+1=26&rowAgent+1=21);
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=15&rowAgent+1=0) | (colAgent-1=16&rowAgent+1=0) | (colAgent-1=17&rowAgent+1=0) | (colAgent-1=18&rowAgent+1=0) | (colAgent-1=19&rowAgent+1=0) | (colAgent-1=20&rowAgent+1=0) | (colAgent-1=21&rowAgent+1=0) | (colAgent-1=22&rowAgent+1=0) | (colAgent-1=23&rowAgent+1=0) | (colAgent-1=24&rowAgent+1=0) | (colAgent-1=25&rowAgent+1=0) | (colAgent-1=26&rowAgent+1=0) | (colAgent-1=0&rowAgent+1=1) | (colAgent-1=26&rowAgent+1=1) | (colAgent-1=0&rowAgent+1=2) | (colAgent-1=26&rowAgent+1=2) | (colAgent-1=0&rowAgent+1=3) | (colAgent-1=26&rowAgent+1=3) | (colAgent-1=0&rowAgent+1=4) | (colAgent-1=26&rowAgent+1=4) | (colAgent-1=0&rowAgent+1=5) | (colAgent-1=26&rowAgent+1=5) | (colAgent-1=0&rowAgent+1=6) | (colAgent-1=26&rowAgent+1=6) | (colAgent-1=0&rowAgent+1=7) | (colAgent-1=26&rowAgent+1=7) | (colAgent-1=0&rowAgent+1=8) | (colAgent-1=26&rowAgent+1=8) | (colAgent-1=0&rowAgent+1=9) | (colAgent-1=26&rowAgent+1=9) | (colAgent-1=0&rowAgent+1=10) | (colAgent-1=26&rowAgent+1=10) | (colAgent-1=0&rowAgent+1=11) | (colAgent-1=26&rowAgent+1=11) | (colAgent-1=0&rowAgent+1=12) | (colAgent-1=26&rowAgent+1=12) | (colAgent-1=0&rowAgent+1=13) | (colAgent-1=26&rowAgent+1=13) | (colAgent-1=0&rowAgent+1=14) | (colAgent-1=26&rowAgent+1=14) | (colAgent-1=0&rowAgent+1=15) | (colAgent-1=26&rowAgent+1=15) | (colAgent-1=0&rowAgent+1=16) | (colAgent-1=26&rowAgent+1=16) | (colAgent-1=0&rowAgent+1=17) | (colAgent-1=26&rowAgent+1=17) | (colAgent-1=0&rowAgent+1=18) | (colAgent-1=26&rowAgent+1=18) | (colAgent-1=0&rowAgent+1=19) | (colAgent-1=26&rowAgent+1=19) | (colAgent-1=0&rowAgent+1=20) | (colAgent-1=26&rowAgent+1=20) | (colAgent-1=0&rowAgent+1=21) | (colAgent-1=1&rowAgent+1=21) | (colAgent-1=2&rowAgent+1=21) | (colAgent-1=3&rowAgent+1=21) | (colAgent-1=4&rowAgent+1=21) | (colAgent-1=5&rowAgent+1=21) | (colAgent-1=6&rowAgent+1=21) | (colAgent-1=7&rowAgent+1=21) | (colAgent-1=8&rowAgent+1=21) | (colAgent-1=9&rowAgent+1=21) | (colAgent-1=10&rowAgent+1=21) | (colAgent-1=11&rowAgent+1=21) | (colAgent-1=12&rowAgent+1=21) | (colAgent-1=13&rowAgent+1=21) | (colAgent-1=14&rowAgent+1=21) | (colAgent-1=15&rowAgent+1=21) | (colAgent-1=16&rowAgent+1=21) | (colAgent-1=17&rowAgent+1=21) | (colAgent-1=18&rowAgent+1=21) | (colAgent-1=19&rowAgent+1=21) | (colAgent-1=20&rowAgent+1=21) | (colAgent-1=21&rowAgent+1=21) | (colAgent-1=22&rowAgent+1=21) | (colAgent-1=23&rowAgent+1=21) | (colAgent-1=24&rowAgent+1=21) | (colAgent-1=25&rowAgent+1=21) | (colAgent-1=26&rowAgent+1=21);
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=15&rowAgent=0) | (colAgent-1=16&rowAgent=0) | (colAgent-1=17&rowAgent=0) | (colAgent-1=18&rowAgent=0) | (colAgent-1=19&rowAgent=0) | (colAgent-1=20&rowAgent=0) | (colAgent-1=21&rowAgent=0) | (colAgent-1=22&rowAgent=0) | (colAgent-1=23&rowAgent=0) | (colAgent-1=24&rowAgent=0) | (colAgent-1=25&rowAgent=0) | (colAgent-1=26&rowAgent=0) | (colAgent-1=0&rowAgent=1) | (colAgent-1=26&rowAgent=1) | (colAgent-1=0&rowAgent=2) | (colAgent-1=26&rowAgent=2) | (colAgent-1=0&rowAgent=3) | (colAgent-1=26&rowAgent=3) | (colAgent-1=0&rowAgent=4) | (colAgent-1=26&rowAgent=4) | (colAgent-1=0&rowAgent=5) | (colAgent-1=26&rowAgent=5) | (colAgent-1=0&rowAgent=6) | (colAgent-1=26&rowAgent=6) | (colAgent-1=0&rowAgent=7) | (colAgent-1=26&rowAgent=7) | (colAgent-1=0&rowAgent=8) | (colAgent-1=26&rowAgent=8) | (colAgent-1=0&rowAgent=9) | (colAgent-1=26&rowAgent=9) | (colAgent-1=0&rowAgent=10) | (colAgent-1=26&rowAgent=10) | (colAgent-1=0&rowAgent=11) | (colAgent-1=26&rowAgent=11) | (colAgent-1=0&rowAgent=12) | (colAgent-1=26&rowAgent=12) | (colAgent-1=0&rowAgent=13) | (colAgent-1=26&rowAgent=13) | (colAgent-1=0&rowAgent=14) | (colAgent-1=26&rowAgent=14) | (colAgent-1=0&rowAgent=15) | (colAgent-1=26&rowAgent=15) | (colAgent-1=0&rowAgent=16) | (colAgent-1=26&rowAgent=16) | (colAgent-1=0&rowAgent=17) | (colAgent-1=26&rowAgent=17) | (colAgent-1=0&rowAgent=18) | (colAgent-1=26&rowAgent=18) | (colAgent-1=0&rowAgent=19) | (colAgent-1=26&rowAgent=19) | (colAgent-1=0&rowAgent=20) | (colAgent-1=26&rowAgent=20) | (colAgent-1=0&rowAgent=21) | (colAgent-1=1&rowAgent=21) | (colAgent-1=2&rowAgent=21) | (colAgent-1=3&rowAgent=21) | (colAgent-1=4&rowAgent=21) | (colAgent-1=5&rowAgent=21) | (colAgent-1=6&rowAgent=21) | (colAgent-1=7&rowAgent=21) | (colAgent-1=8&rowAgent=21) | (colAgent-1=9&rowAgent=21) | (colAgent-1=10&rowAgent=21) | (colAgent-1=11&rowAgent=21) | (colAgent-1=12&rowAgent=21) | (colAgent-1=13&rowAgent=21) | (colAgent-1=14&rowAgent=21) | (colAgent-1=15&rowAgent=21) | (colAgent-1=16&rowAgent=21) | (colAgent-1=17&rowAgent=21) | (colAgent-1=18&rowAgent=21) | (colAgent-1=19&rowAgent=21) | (colAgent-1=20&rowAgent=21) | (colAgent-1=21&rowAgent=21) | (colAgent-1=22&rowAgent=21) | (colAgent-1=23&rowAgent=21) | (colAgent-1=24&rowAgent=21) | (colAgent-1=25&rowAgent=21) | (colAgent-1=26&rowAgent=21);
formula AgentIsOnLava = (colAgent=16&rowAgent=1) | (colAgent=17&rowAgent=1) | (colAgent=18&rowAgent=1) | (colAgent=19&rowAgent=1) | (colAgent=16&rowAgent=2) | (colAgent=17&rowAgent=2) | (colAgent=18&rowAgent=2) | (colAgent=19&rowAgent=2) | (colAgent=10&rowAgent=3) | (colAgent=11&rowAgent=3) | (colAgent=12&rowAgent=3) | (colAgent=10&rowAgent=4) | (colAgent=11&rowAgent=4) | (colAgent=12&rowAgent=4) | (colAgent=10&rowAgent=5) | (colAgent=11&rowAgent=5) | (colAgent=12&rowAgent=5) | (colAgent=10&rowAgent=6) | (colAgent=11&rowAgent=6) | (colAgent=12&rowAgent=6) | (colAgent=16&rowAgent=7) | (colAgent=17&rowAgent=7) | (colAgent=18&rowAgent=7) | (colAgent=19&rowAgent=7) | (colAgent=20&rowAgent=7) | (colAgent=21&rowAgent=7) | (colAgent=22&rowAgent=7) | (colAgent=23&rowAgent=7) | (colAgent=16&rowAgent=8) | (colAgent=17&rowAgent=8) | (colAgent=18&rowAgent=8) | (colAgent=19&rowAgent=8) | (colAgent=20&rowAgent=8) | (colAgent=21&rowAgent=8) | (colAgent=22&rowAgent=8) | (colAgent=23&rowAgent=8) | (colAgent=16&rowAgent=9) | (colAgent=17&rowAgent=9) | (colAgent=18&rowAgent=9) | (colAgent=19&rowAgent=9) | (colAgent=20&rowAgent=9) | (colAgent=21&rowAgent=9) | (colAgent=22&rowAgent=9) | (colAgent=23&rowAgent=9) | (colAgent=16&rowAgent=10) | (colAgent=17&rowAgent=10) | (colAgent=18&rowAgent=10) | (colAgent=19&rowAgent=10) | (colAgent=20&rowAgent=10) | (colAgent=21&rowAgent=10) | (colAgent=22&rowAgent=10) | (colAgent=23&rowAgent=10) | (colAgent=8&rowAgent=11) | (colAgent=9&rowAgent=11) | (colAgent=10&rowAgent=11) | (colAgent=11&rowAgent=11) | (colAgent=12&rowAgent=11) | (colAgent=16&rowAgent=11) | (colAgent=17&rowAgent=11) | (colAgent=18&rowAgent=11) | (colAgent=19&rowAgent=11) | (colAgent=20&rowAgent=11) | (colAgent=21&rowAgent=11) | (colAgent=22&rowAgent=11) | (colAgent=23&rowAgent=11) | (colAgent=8&rowAgent=12) | (colAgent=9&rowAgent=12) | (colAgent=10&rowAgent=12) | (colAgent=11&rowAgent=12) | (colAgent=12&rowAgent=12) | (colAgent=8&rowAgent=13) | (colAgent=9&rowAgent=13) | (colAgent=10&rowAgent=13) | (colAgent=11&rowAgent=13) | (colAgent=12&rowAgent=13) | (colAgent=8&rowAgent=14) | (colAgent=9&rowAgent=14) | (colAgent=10&rowAgent=14) | (colAgent=11&rowAgent=14) | (colAgent=12&rowAgent=14) | (colAgent=22&rowAgent=14) | (colAgent=23&rowAgent=14) | (colAgent=24&rowAgent=14) | (colAgent=25&rowAgent=14) | (colAgent=8&rowAgent=15) | (colAgent=9&rowAgent=15) | (colAgent=10&rowAgent=15) | (colAgent=11&rowAgent=15) | (colAgent=12&rowAgent=15) | (colAgent=22&rowAgent=15) | (colAgent=23&rowAgent=15) | (colAgent=24&rowAgent=15) | (colAgent=25&rowAgent=15) | (colAgent=8&rowAgent=16) | (colAgent=9&rowAgent=16) | (colAgent=10&rowAgent=16) | (colAgent=11&rowAgent=16) | (colAgent=12&rowAgent=16) | (colAgent=22&rowAgent=16) | (colAgent=23&rowAgent=16) | (colAgent=24&rowAgent=16) | (colAgent=25&rowAgent=16) | (colAgent=22&rowAgent=17) | (colAgent=23&rowAgent=17) | (colAgent=24&rowAgent=17) | (colAgent=25&rowAgent=17);
formula AgentIsOnGoal = (colAgent=25&rowAgent=10);
init
  true
endinit


module Agent
  colAgent : [1..25];
  rowAgent : [1..20];
  viewAgent : [0..3];

  [Agent_turn_right] !AgentIsOnSlippery &  !AgentIsOnLava &true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] !AgentIsOnSlippery &  !AgentIsOnLava &viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] !AgentIsOnSlippery &  !AgentIsOnLava &viewAgent=0 -> 1.000000: (viewAgent'=3);
  [Agent_move_North] viewAgent=3 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveNorthWall -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_East] viewAgent=0 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveEastWall -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveSouthWall -> 1.000000: (rowAgent'=rowAgent+1);
  [Agent_move_West] viewAgent=2 & !AgentIsOnSlippery & !AgentIsOnLava & !AgentIsOnGoal & !AgentCannotMoveWestWall -> 1.000000: (colAgent'=colAgent-1);
  [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);
  [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);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & AgentCannotSlipNorthEast & !AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & !AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorth & AgentCannotSlipNorth & AgentCannotSlipNorthEast & AgentCannotSlipNorthWest -> true;
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & !AgentCannotSlipWest & !AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & AgentCannotSlipWest & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & !AgentCannotSlipWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorth & AgentCannotSlipWest & AgentCannotSlipNorthWest -> true;
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & !AgentCannotSlipEast & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & AgentCannotSlipEast & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & !AgentCannotSlipEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorth & AgentCannotSlipEast & AgentCannotSlipNorthEast -> true;
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorth & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: true;
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorth & AgentCannotSlipSouth -> 1.000000: true;
  [Agent_turn_right] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (rowAgent'=rowAgent-1);
  [Agent_turn_right] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (rowAgent'=rowAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyNorth & !AgentCannotSlipNorth & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (rowAgent'=rowAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyNorth & AgentCannotSlipNorth & viewAgent=0 -> 1.000000: (viewAgent'=3);
  [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);
  [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);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipNorthEast -> true;
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyEast & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> true;
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & !AgentCannotSlipSouth & !AgentCannotSlipSouthEast -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & AgentCannotSlipSouth & !AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & !AgentCannotSlipSouth & AgentCannotSlipSouthEast -> 1.000000: (rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyEast & AgentCannotSlipSouth & AgentCannotSlipSouthEast -> true;
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyEast & !AgentCannotSlipEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: true;
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyEast & AgentCannotSlipEast -> 1.000000: true;
  [Agent_turn_right] AgentIsOnSlipperyEast & !AgentCannotSlipEast & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (colAgent'=colAgent+1);
  [Agent_turn_right] AgentIsOnSlipperyEast & AgentCannotSlipEast & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] AgentIsOnSlipperyEast & !AgentCannotSlipEast & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (colAgent'=colAgent+1);
  [Agent_turn_left] AgentIsOnSlipperyEast & !AgentCannotSlipEast & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (colAgent'=colAgent+1);
  [Agent_turn_left] AgentIsOnSlipperyEast & AgentCannotSlipEast & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyEast & AgentCannotSlipEast & viewAgent=0 -> 1.000000: (viewAgent'=3);
  [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);
  [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);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & !AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & AgentCannotSlipSouthEast & !AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent-1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth & AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & !AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperySouth & AgentCannotSlipSouth & AgentCannotSlipSouthEast & AgentCannotSlipSouthWest -> true;
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & !AgentCannotSlipWest & !AgentCannotSlipSouthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & AgentCannotSlipWest & !AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & !AgentCannotSlipWest & AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperySouth & AgentCannotSlipWest & AgentCannotSlipSouthWest -> true;
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & !AgentCannotSlipEast & !AgentCannotSlipSouthEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & AgentCannotSlipEast & !AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & !AgentCannotSlipEast & AgentCannotSlipSouthEast -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperySouth & AgentCannotSlipEast & AgentCannotSlipSouthEast -> true;
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperySouth & !AgentCannotSlipSouth -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: true;
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperySouth & AgentCannotSlipSouth -> 1.000000: true;
  [Agent_turn_right] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (rowAgent'=rowAgent+1);
  [Agent_turn_right] AgentIsOnSlipperySouth & AgentCannotSlipSouth & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (rowAgent'=rowAgent+1);
  [Agent_turn_left] AgentIsOnSlipperySouth & !AgentCannotSlipSouth & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (rowAgent'=rowAgent+1);
  [Agent_turn_left] AgentIsOnSlipperySouth & AgentCannotSlipSouth & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] AgentIsOnSlipperySouth & AgentCannotSlipSouth & viewAgent=0 -> 1.000000: (viewAgent'=3);
  [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);
  [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);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & !AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & AgentCannotSlipSouthWest & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & !AgentCannotSlipWest & AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & !AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyWest & AgentCannotSlipWest & AgentCannotSlipSouthWest & AgentCannotSlipNorthWest -> true;
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthWest -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & AgentCannotSlipNorth & !AgentCannotSlipNorthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & !AgentCannotSlipNorth & AgentCannotSlipNorthWest -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyWest & AgentCannotSlipNorth & AgentCannotSlipNorthWest -> true;
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & !AgentCannotSlipSouth & !AgentCannotSlipSouthWest -> 0.950000: (rowAgent'=rowAgent+1) + 0.050000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & AgentCannotSlipSouth & !AgentCannotSlipSouthWest -> 1.000000: (colAgent'=colAgent-1)&(rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & !AgentCannotSlipSouth & AgentCannotSlipSouthWest -> 1.000000: (rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyWest & AgentCannotSlipSouth & AgentCannotSlipSouthWest -> true;
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyWest & !AgentCannotSlipWest -> 0.950000: (colAgent'=colAgent-1) + 0.050000: true;
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyWest & AgentCannotSlipWest -> 1.000000: true;
  [Agent_turn_right] AgentIsOnSlipperyWest & !AgentCannotSlipWest & true -> 0.950000: (viewAgent'=mod(viewAgent+1,4)) + 0.050000: (colAgent'=colAgent-1);
  [Agent_turn_right] AgentIsOnSlipperyWest & AgentCannotSlipWest & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] AgentIsOnSlipperyWest & !AgentCannotSlipWest & viewAgent>0 -> 0.950000: (viewAgent'=viewAgent-1) + 0.050000: (colAgent'=colAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyWest & !AgentCannotSlipWest & viewAgent=0 -> 0.950000: (viewAgent'=3) + 0.050000: (colAgent'=colAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyWest & AgentCannotSlipWest & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyWest & AgentCannotSlipWest & viewAgent=0 -> 1.000000: (viewAgent'=3);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast -> 0.950000: (colAgent'=colAgent+1) + 0.050000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_East] viewAgent=0 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast -> 1.000000: true;
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipNorth -> 0.950000: (rowAgent'=rowAgent-1) + 0.050000: (colAgent'=colAgent+1)&(rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipNorth -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipNorth -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_North] viewAgent=3 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipNorth -> 1.000000: true;
  [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);
  [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);
  [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);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1) + 0.500000: (colAgent'=colAgent+1);
  [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);
  [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);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [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);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 0.500000: (colAgent'=colAgent+1) + 0.500000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.051724: (colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & !AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 0.982759: (rowAgent'=rowAgent+1) + 0.051724: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & !AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent+1)&(colAgent'=colAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & !AgentCannotSlipSouth -> 1.000000: (rowAgent'=rowAgent+1);
  [Agent_move_South] viewAgent=1 & AgentIsOnSlipperyNorthEast & AgentCannotSlipNorthEast & AgentCannotSlipEast & AgentCannotSlipSouthEast & AgentCannotSlipSouth -> 1.000000: true;
  [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);
  [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);
  [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);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  [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);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.982759: (colAgent'=colAgent-1) + 0.051724: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & !AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (colAgent'=colAgent-1);
  [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);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1) + 0.500000: (rowAgent'=rowAgent-1);
  [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);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & !AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 0.500000: (rowAgent'=rowAgent-1) + 0.500000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & !AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & !AgentCannotSlipNorthEast -> 1.000000: (rowAgent'=rowAgent-1)&(colAgent'=colAgent+1);
  [Agent_move_West] viewAgent=2 & AgentIsOnSlipperyNorthEast & AgentCannotSlipWest & AgentCannotSlipNorthWest & AgentCannotSlipNorth & AgentCannotSlipNorthEast -> 1.000000: true;
  [Agent_turn_right] AgentIsOnSlipperyNorthEast & true & true -> 1.000000: (viewAgent'=mod(viewAgent+1,4));
  [Agent_turn_left] AgentIsOnSlipperyNorthEast & true & viewAgent>0 -> 1.000000: (viewAgent'=viewAgent-1);
  [Agent_turn_left] AgentIsOnSlipperyNorthEast & true & viewAgent=0 -> 1.000000: (viewAgent'=3);
endmodule