An elegant model of how pacman moves around a mazes, avoids walls, eats food, and sometimes gets eaten by Blinky the ghost. The model is very readable, although there is not any explicit supporting documentation.