(last update: Fri Nov 27 19:28:25 CET 2015)
If you want to install SPIN at home, you can download precompiled binaries for various operating systems. Remember that you can always ssh -X to the computers in room F204.
In a Debian session, open a terminal.
Create a folder in your home directory where you will install SPIN, for instance ~/bin:
mkdir ~/bin
Add that folder to your $PATH variable. For instance, add the following line to your ~/.bashrc file:
export PATH=$PATH:$HOME/bin
Download to ~/bin the SPIN tool and its graphical interface:
cd ~/bin/ wget 'http://spinroot.com/spin/Bin/spin644_linux32.gz' wget 'http://spinroot.com/spin/Src/ispin.tcl' gunzip spin644_linux32.gz ln -s spin644_linux32 spin chmod 755 spin644_linux32 chmod 755 ispin.tcl
SPIN is now installed in your machine. On the terminal:
The SPIN release that you have previously installed is a 32 bits program. Machines in the room F204 are 64 bits. To use SPIN from the graphical interface ispin.tcl we need to use a modified version of the ispin.tcl program. Download it and install it as follows:
cd ~/bin wget https://lipn.univ-paris13.fr/~rodriguez/teach/sdsc/2015-16/files/ispin-F204.tcl chmod 755 ispin-F204.tcl
From now, instead of using ispin.tcl, use ispin-F204.tcl.
NOTE: Currently, SPIN only works in the F204 machines. If you are physically using a machine in another room, F205, F206... use ssh -X to remotely execute spin and ispin-F204-tcl in some machine of the room F204. For instance, we execute SPIN on the machine F204-1 while being physically logged on machine F206-3:
user@F206-3:~$ ssh -X F204-1 user@f204-1's password: Linux F204-1 3.2.0-4-amd64 #1 SMP Debian 3.2.68-1+deb7u6 x86_64 [...] user@F204-1:~$ spin Spin Version 6.4.4 -- 1 November 2015 spin: error, no filename specified user@F204-1:~$ user@F204-1:~$ ispin-F204.tcl [...]
Nothing changes.
Use the following commands instead of the ones given in the slides (the only difference is the -m32):
spin -a programme.pml gcc -m32 pan.c -o pan ./pan -E spin -t programme.pml
Here you have a Makefile for automating the commands to use spin. Before using it, you need to modify the variable T (for target) in the makefile to point to your Promela file, for instance test.pml:
T=test.pml
After that, use the following:
NOTE: make ver calls pan with option -a, which makes SPIN check for LTL properties but disables the verification of assertions. Remove the -a in the Makefile to check for assertions.