main.pdf372.01 KB
Bodin has applied SPIN to solve puzzles like the Japanese river puzzle, an advanced version of the famous wolf-goat-cabbage puzzle. Defining a Promela model can become cumbersome and debugging can be very time-consuming, since SPIN does the syntax check (e.g. type checking) only at runtime and developers might have decided...