Formal Methods for Software Development TDA294/DIT271, LP1, HT2017

Additional Installation Notes for Spin and jSpin

Personal Linux system (tested for Ubuntu / Debian)

Spin requires yacc (in most distributions found in the bison package) and libc6-dev. The following commands should allow you to install the currently latest version of spin.

~$ sudo apt-get install bison libc6-dev
~$ cd /tmp
/tmp$ wget
/tmp$ tar xzf spin645.tar.gz
/tmp$ cd Spin
/tmp/Spin$ cd Src6.4.5
/tmp/Spin/Src6.4.3$ make
/tmp/Spin/Src6.4.3$ sudo cp spin /usr/local/bin/spin
/tmp/Spin/Src6.4.3$ spin
Spin Version 6.4.5 -- 1 January 2016
spin: error, no filename specified

jSpin is written in Java and thus cross-platform, but requires some small changes to be run under Linux since the default configuration file is for Windows. We provide a slightly modified version. The SpinSpider fearture of jSpin requires dot (in most distributions found in the graphviz package).

~/myjspinfolder$ sudo apt-get install graphviz
~/myjspinfolder$ wget -U Mozilla/5.0
~/myjspinfolder$ unzip 
~/myjspinfolder$ rm config.cfg
~/myjspinfolder$ wget
~/myjspinfolder$ java -jar jspin.jar

Note that new config.cfg file assumes that spin, gcc, and dot are in your PATH. If you experience problems, put full paths in config.cfg.

To simplify navigation to Promela files, you may consider to change in the (new) config.cfg file the directory name jspin-examples in the line
to the directory where you have your promela files.

Remote Chalmers servers

We provide precompiled binaries for the remote11/ machines. You can connect to a remote server using ssh, use the -X flag if you want to use the jSpin GUI.

~$ ssh -X
user@remote12:~$ mkdir jspin
user@remote12:~$ cd jspin
user@remote12:~/jspin$ cd jspin
user@remote12:~/jspin$ wget
user@remote12:~/jspin$ unzip
user@remote12:~/jspin$ export PATH=$PATH:`pwd`/spin4remote/bin
user@remote12:~/jspin$ spin
Spin Version 6.1.0 -- 2 May 2011
spin: error, no filename specified
user@remote12:~/jspin$ java -jar spin4remote/bin/jspin.jar

Additional hints for Spin on MacOSX

If you get the following message sh: /lib/cpp: No such file or directory when running 'spin' you can do the following: Find out where your cpp is installed via which cpp (using the Terminal application) (you might need to install XCode from Apple's MacOSX DVDs first or for free on the AppStore if you are using Lion). Then enter the following in the Terminal (press enter after each line)
sudo mkdir /lib
ln -s path_to_cpp/cpp /lib/cpp
alternatively you can patch spins sourcecode and change the line in main.c from /lib/cpp to cpp.

Hints for jSpin usage

After downloading and unpacking, jSpin can be directly executed. Documentation including installation manual is in doc/jspin-user.pdf

You can run jSpin with java -jar jspin.jar. However, it is recommended to put a corresponding script somewhere in your PATH. For Windows, you can copy the run.bat from the jSpin distribution (better renaming it to something more specific), and within the script expand jspin.jar with its full path. For UNIX, you can use the script jspin, but replace PATHTOJSPIN by the true path to jspin.jar.

In order for SpinSpider (part of jSpin) to draw state diagrams, the DOT tool needs to be installed. (It is part of the graphviz package.)

Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt, Aug 21, 2017