Software Engineering using Formal Methods |
TDA293/DIT270, LP1, HT2015 |
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 http://spinroot.com/spin/Src/spin643.tar.gz /tmp $ tar xzf spin643.tar.gz /tmp $ cd Spin /tmp/Spin $ cd Src6.4.3 /tmp/Spin/Src6.4.3 $ make /tmp/Spin/Src6.4.3 $ sudo cp spin /usr/local/bin/spin /tmp/Spin/Src6.4.3 $ spin pin Version 6.4.3 -- 16 December 2014 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). ~/myfolder $ sudo apt-get install graphviz ~/myfolder $ wget http://www.weizmann.ac.il/sci-tea/benari/software/jspin/jspin-5-0.zip ~/myfolder $ unzip jspin-5-0.zip ~/myfolder $ rm config.cfg ~/myfolder $ wget http://www.cse.chalmers.se/edu/course/TDA293/jspincfg/config.cfg ~/myfolder $ 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
Remote Chalmers servers We provide precompiled binaries for the remote11/remote12.chalmers.se 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.chalmers.se user@remote12:~ $ mkdir jspin user@remote12:~ $ cd jspin user@remote12:~/jspin $ cd jspin user@remote12:~/jspin $ wget http://www.cse.chalmers.se/edu/course/TDA293/spin4remote.zip user@remote12:~/jspin $ unzip spin4remote.zip 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) 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 , Sep 8, 2015 |