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 to use general-purpose editors, from which they do not get any support when editing Promela models.
The purpose of the work described in this paper is twofold. Firstly, it addresses the lack of rich editors for Promela models. Thus, an Eclipse-editor has been defined based on Xtext, which is able to assist the developer of Promela models and which comes with rich features such as auto-completion, syntax highlighting, and rename refactoring. Together with a shell script to start SPIN on the edited model, this editor enables the developer to work with Promela models efficiently.
Secondly, a domain-specific language (DSL) has been developed based on Xtext that allows us to formulate river-crossing puzzles in a very intuitive way. The DSL comes with a rich Eclipse-editor as well as with a code generator, which generates the corresponding Promela model as input for the model checker.