Spin is distributed in source form to encourage research in formal verification, and to help a support friendly and open exchange of algorithms, ideas, and tools. The software itself has a copyright from Lucent Technologies and Bell Laboratories, and is distributed for research and educational purposes only (i.e., no guarantee of any kind is implied by the distribution of the code, and all rights are reserved by the copyright holder). For this general use of Spin, no license is required.
Commercial application of the Spin software is also allowed, but requires the acceptance of a basic license. Refer to the Spin Public license for details.
All binaries have an extension that matches the Spin version number, such as spin422.exe. To install the binary, rename it to spin.exe and copy it into your bin directory.
If you have machine type that is not available there, or if you are installing Spin for the first time, then follow the more detailed instructions below.
gunzip *.tar.gz tar -xf *.tar cd Src* make -f make_unix
If you are on a SOLARIS system, edit the makefile and add -DSOLARIS to the compiler directives in the makefile before you type 'make'. Similarly, if you use a different C compiler than defined in the makefile, edit the makefile first. You need to have at least a C compiler and a copy of yacc.
Spin should compile without warnings. Install the executable version of spin in a directory that is within your default search path (such as your home bin directory, or /usr/local/bin etc.)
If all else fails, you can also compile everything with the following line:
yacc -v -d spin.y; cc -o spin *.cOn Unix systems Spin assumes that the standard C preprocessor cpp is stored in file "/lib/cpp". On some systems this is different: check the comments in the makefile for details if you run into this problem.
The current version of Xspin is compatible with
Tk version 4.2 - Tcl version 7.6 Tk version 8.4 - Tcl version 8.4
Xspin prints the version numbers of Spin, Xspin, and Tcl/Tk when it starts up. You can also check separately which version of Tcl/Tk you have installed by executing the following commands in `wish' (a Tcl/Tk command):
info tclversion puts $tk_versionYou can find out which version of Spin you have by typing, at a Unix command prompt:
$ spin -V
Xspin can also make use the graph layout program 'dot' if it is available on your system (not required, but very nice if available -- xspin will automatically recognize if it is installed.) For information on 'dot,' see Related software.
To install Xspin on Unix:
cp xspin422.tcl /usr/local/bin/xspin chmod +x /usr/local/bin/xspin
xspin # or xspin.tcl if you keep the extension... or xspin promela_spec For example: cd Test xspin leader
If you use Spin from the command line (i.e., without Xspin), be warned that some command shells, e.g., the MKS Korn-shell, have none-standard rules for argument parsing (i.e., you can not reliably quote an argument that contains spaces, such as an LTL formula). In most cases this will not be much of a problem, except with the conversion of LTL formula with the Spin -f option. You can circumvent this by using -F instead of -f, to read the formula from a file instead of the command line.
To run Spin, even from the precompiled version, you need a working C-compiler and a C-preprocessor, because Spin generates its model checking software as C-source files that require compilation before a verification can be performed. This guarantees fast model checking, because each model checker can be optimized to the specific model being checked. Check, for instance, if you can compile and run a minimal C program succesfully, e.g.:
#include <stdio.h>
int main(void) { printf("hello\n"); }
To find a public version of a C compiler and some instructions on how to install it see Related software.
The xspin*.tcl source is contained in the .zip file of the distribution. Copy the .tcl file as is into a directory where you plan to work, or put a shortcut to this file on the Desktop or in the Start Menu. If you keep the extension .tcl, make sure it is recognized as a 'wish' file by the system, so that xspin starts when you double click the xspin*.tcl script.
Under cygwin, copy the xspin*.tcl file to /bin/xspin and make it executable -- check the first few lines of xspin*.tcl to make sure the location of xspin matches what you have on your system (it is currently setup for c:/cygwin/bin/xspin). You can now use xspin as a normal Unix-style command, and you can pass the name of a filename to it, for instance as:
xspin leader
An indirect way to force xspin to startup is to first start `wish' from the Start Menu, under Programs, then select the larger window that comes up (the command window), and cd to the directory where you've stored the xspin.tcl file. Then you can then start it up by typing:
source xspin.tcl # or whatever else you've named thisand you should be up and running.
The PC installation assumes that you have a command called "cpp.exe" available (which comes with the gnu-c installation), which is the traditional name of the C preprocessor. Alternatively, it can also use the Visual C++ compiler, which is named cl.exe for preprocessing. To complicate your life somewhat, if you have a copy of the Borland C++ compiler installed, you'll notice that this cplusplus compiler was also named cpp.exe -- that's not the cpp you want. To avoid the name clash, you either have to edit the Spin source code to give it the full path name of the 'real' cpp.exe and recompile, or use Spin with the command-line option -Pxxxx where xxxx is the path for cpp.exe. Nothing much in Spin will work without access to cpp.exe. You can do a reasonable number of things without gcc.exe though (like simulations). The C-compiler is required for all verifications and for the automata views in Xspin.
The C preprocessor on Mac OS X cannot be found in /lib. Change the path in the make_unix makefile for the proper location (/usr/bin/cpp), and in addition also tell the Mac preprocessor to handle its input as "assembler-with-cpp." This can be done by adding a flag to cpp, for instance in the make_unix by adding the directive
-DCPP="\"/usr/bin/cpp -xassembler-with-cpp\""to the definition of CFLAGS.
http://www.maths.mq.edu.au/~steffen/tcltk/TclTkAqua/
Xspin by default places its temporary files into the root directory. This is nasty if you have admin privileges and probably leads to error messages if you don't. To prevent this, add a "cd" statement to xspin (no arguments, just cd by itself on a line), as the first command executed. Place it, for instance, directly after the opening comments in the file. This makes Xspin use the home directory for these files.
TclTk Aqua also provides the possibility to start a script when being run. For instance, to make Xspin start if you launch the TCL interpreter: move the xspin file into the "Wish Shell.app", as follows:
chmod -R u+w Wish\ Shell.app mkdir Wish\ Shell.app/Contents/Resources/Scripts mv xspin*.tcl Wish\ Shell.app/Contents/Resources/Scripts/AppMain.tcl
ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.ZA copy of this file is also available in: http://spinroot.com/spin/Bin/index.html (You don't need yacc on the PC's if you use the pre-compiled version of Spin for the pc in the pc*.zip file from the distribution) Look at the file make_it.bat for an example on how to perform the compilation.
http://www.research.att.com/sw/tools/graphviz/The are both PC and Unix versions of Dot available. For documentation of Dot see:
A Technique for Drawing Directed Graphs, by Gansner, Koutsofios, North and Vo, IEEE-TSE, March, 1993.
http://stwww.weizmann.ac.il/g-cs/benari/jspin/
http://spinroot.com/spin/Src/ltl2ba.tar.gzOr can be obtained from the authors website via:
http://verif.liafa.jussieu.fr/ltl2ba/The C source code can easily be linked with Spin, or run as a standalone tool.
An alternative converter is the ``Temporal Massage Parlor'' written by Kousha Etessami. This translator is written in ML, and is also available in source form via
http://www.bell-labs.com/topic/swdist/
| Spin HomePage | (Page Last Updated: 12 December 2004) |