COMP60611 jSpin Reference Sheet
References
The Spin website, contains detailed installation instructions and man pages for both Spin and Promela as well as much other useful material.
This page contains pointers to the manual pages for Promela and other useful background information.
The book Principles of the Spin Model Checker is highly recommended as an introduction to Spin, jSpin and the Promela modelling language. The first three chapters provide a good overview and are recommended reading as you begin to use jSpin. This book is available for download as an electronic resource from the John Rylands library.
Installation
It is highly recommended that you create your own subdirectory in the jspin-examples directory of the jSpin distribution to keep your Promela files. This avoids certain ‘path’ problems sometimes encountered if you keep your own Promela files in other directories.
Windows installation
You will need to install jspin and mingw, which provides the C compiler needed by Spin.
Goto:
and download and run the following installer files. Selecting default installation options works fine.
jspin-5-0.exe The jSpin WIndows installer
mingw.exe The MinGW single file installer
After installing the above two packages, everything should be ok!
You can run jSpin by double clicking on the icon installed on the desktop.
You can test the installation by Opening one of the example files using the Open button (say second.pml) and then pressing the Verify button (you should get output in the right hand pane saying that there is 1 error in the verification).
If you have any problems installing jSpin and Spin, please ask us to help!!
Linux installation
To install under Linux on the machines in the lab, download the following file from the jspin website.
jspin-5-0.zip
Extract the contents into a new directory in your ‘home’ (I use a directory called jspinHome).
Download the Linux spin executable (32bit version) from
The downloaded file will be called spin610_linux; this is the linux executable file.
In your jspin home directory, create a directory called ‘bin’.
Copy the spin executable into the bin directory
Rename the executable ‘spin.exe’ (mv spin610_linux spin.exe)
Make the file executable (for example, chmod a+x spin.exe)
In you jspin home directory, edit the following entries in the file ‘config.cfg’ to read as follows:
- SPIN=[The absolute path to the spin.exefile, i.e. something like: /home/…./bin/spin.exe](or whatever you called the executable)
- C_COMPILER=gcc
- DOT=/usr/bin/dot
Run jSpin from your jspin home directory by entering the command:
java –jar jspin.jar&
You can test the installationas described for the Windows installation.
If you have any problems installing jSpin and Spin, please ask us to help!!
Other installations
If you wish to install jSpin etc. on your laptop and you run an operating system other than the above, please follow the links on the spinroot website which may be able to point you in the right direction. Please ask for advice from us if you hit problems (though we can’t guarantee to solve them).