Spin for puzzles: Using Spin for solving the Japanese river puzzle and the Square-1 cube

This paper describes how the SPIN model checker can be applied to solving puzzles, such as riverIQGame (an advanced “wolf, goat and cabbage” puzzle) or “Irregular IQ Cube” (also known as ‘Square-1’).