Lab Session with Spin and Modex
Online material for a short course presented at
the Fourth Summer School on Formal Techniques,
held May 19-23, 2014, at Menlo College, Atherton, CA, organized by SRI.
- Make sure you have a C compiler installed on your system.
Generally that will be gcc.
- Download spinlab.tar.gz (68K).
Create a directory where you want to do the exercises,
and unpack the file there. For instance:
$ mkdir Summer_2014
$ cd Summer_2014
$ tar -xzf spinlab.tar.gz
- Download the executables for the tools you need to perform the exercises.
Choose your operating system and download the corresponding tar file:
Unpack the file and move the four commands that are created, make sure they are executable,
and move them into the bin directory for your system. For instance (assuming Linux 64 bits):
$ tar -xzf linux64.tar.gz
$ chmod +x spin* modex* ispin verify
$ mv spin* modex* ispin verify /usr/local/bin
On a MAC the bin directory would be /usr/bin instead of /usr/local/bin,
and on both MACs and Linux systems you will likely need to use sudo.
(For the windows 64bit executable, just rename it to spin.exe and move it into the bin directory for your system.)
- There are four html files in the SpinLab directory that was
These will guide you through the exercises:
Explore them in the order listed, minimally doing the exercises from the first two files.
All examples that are discussed can be found in sub-directories of SpinLab:
| Spin/Promela files used in 1_Exercises.html:||SpinLab/P/*.pml|
| C source files used in 2_ModelExtraction.html:||SpinLab/C/*.c|
| additional Spin models, for inspiration:||SpinLab/P2/*.pml
| additional Spin models with LTL properties:||SpinLab/P2/LTL/*.pml|
- Optional Extras
- Online Promela/Spin Man Pages