|Formal Methods for Software Development||TDA294/DIT271, LP1, HT2018|
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), gcc, make, and libc6-dev. The following commands should allow you to install the currently latest version of spin.
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).
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.
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, Aug 31, 2018|