Spin - Version 3.2 - April 1998

`SPIN README`

`Overview of this File`

Downloading Spin
Installing Spin
- on Unix systems
- on Windows95/WindowsNT PC's
Related software (gcc, cpp, go32, wish, dot)

This file contains only the specific guidelines for downloading and installing Spin and related software on Unix and Windows platforms. For a general description of Spin, with pointers to:

and related documentation, please refer to Spin's homepage.

The Spin software is distributed, with all sources, through netlib, with mirror sites around the world. The distribution can be loaded via anonymous ftp to netlib.bell-labs.com from directory /netlib/spin or via the following URLs:

The URLs for the files you'll need to install from this location are named more explicitly in the detailed downloading instructions below.

Spin is distributed in source form to encourage and inspire research in the area of formal verification, and to help support friendly and open exchange of ideas. The software itself has a copyright from Lucent Technologies and Bell Laboratories, and is distributed for educational purposes only (i.e., no guarantee of any kind is implied by the distribution of this code, and all rights are reserved by the copyright holder). For educational or research use of Spin, no license is required. Commercial applications do require a simple license from Bell Labs, which carries a small fee. Please contact gerard@research.bell-labs.com for details.

`1. Downloading Spin`

The current version is Spin 3.2, which runs on any Unix workstation or mainframe, as well as on PCs under Windows95 or WindowsNT. To get up and running from scratch you will need to download the following compressed tar-files.

UNIX systems:
download the following tar-file with sources, the graphical interface Xspin, documentation and examples:
- ftp://netlib.bell-labs.com/netlib/spin/spin320.tar.gz
The sources are written in YACC and ANSI standard C. The optional graphical interface to Spin is written in Tcl/Tk. For detailed installation notes see 1a below.
If you already have a version 3 of Spin installed, you may also be able to use the smaller shell script to update these sources:
- ftp://netlib.bell-labs.com/netlib/spin/upgrade3.tar.gz
Windows95 or WindowsNT PC's:
download the following zip file, with a 32-bit precompiled Spin executable, the graphical interface Xspin, and some examples:
- ftp://netlib.bell-labs.com/netlib/spin/pc_spin320.zip
For detailed installation notes see 1b below.

`1a. Installing Spin on a Unix System`

First cd to Src directory from this distribution and type `make'.

Spin should compile without warnings. You do not have to do anything special unless you are on a Solaris system or a PC (in that case, read the comments in the makefile first). 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.)

You may have to adapt the makefile to pick up an ANSI C standard C compiler (for instance, the Gnu C compiler, gcc). (If you need to install gcc, yacc, or Tcl/Tk, see below under: Related Software)

If all else fails, you can also compile everything with the following two lines:


	yacc -v -d spin.y

	cc -o spin *.c

(Spin assumes that the standard C preprocessor cpp is stored in file "/lib/cpp". On some systems this is different. On a Solaris system, for instance, the file is "/usr/ccs/lib/cpp". You can define this by adding the compiler directive -DSOLARIS)

Testing

To test the basic sanity of the Spin executable, cd to the Test directory and follow the instructions in file README.tests

Adding Xspin

Xspin is an optional, but highly recommended, graphical interface to Spin, written in Tcl/Tk. To obtain Tcl/Tk, see Related software below.

The current version of Xspin is compatible with


	Tk version 4.2 - Tcl version 7.6, and

	Tk version 8.0 - Tcl version 8.0

and should be compatible with also some earlier versions of Tcl/Tk.

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_version

You can find out which version of Spin you have by typing, at a Unix command prompt:


	$ spin -V

Unlike older versions of Xspin, all Xspin source is now collected into a single file inside the Xspin directory to simplify installation.

Xspin can also make use the graph layout program 'dot' if it is available on your system (not required, but nice if it's there -- xspin will automatically recognize if 'dot' is installed.) For information on 'dot,' see Related software.

To install Xspin on Unix, cd to directory Xspin3.2 from the distribution,

follow the instructions at the top of the xspin* file. Minimally: change the first line of this file to point to the executable `wish' command on your system that you want to use. If you use another c-compiler than the default (gcc), you should update the global variable CC inside xspin as well. Follow the instructions inside the xspin* file to do so.
copy the file into a directory within your search path and make it executable, for instance:
```
	cp xspin* /usr/local/bin/xspin

	chmod +x /usr/local/bin/xspin
```
make sure that an executable version of `spin' itself is also within your search path, and is up to date (check by trying: spin -V).

On Unix, invoke the program by typing


	xspin

or

	xspin promela_spec



For example:

	xspin Test/leader

Check the online Help menus in xspin for more details on routine use.

`1b. Installing Spin on a Windows95 or WindowsNT PC`

Unzip the compressed file pc*.zip, and copy spin.exe into a directory with executables that is in your search path.

If you run Spin from the system prompt (i.e., if you're not using Xspin), use the standard MS-DOS prompt. If you use the Korn-shell from, for instance, the MKS toolkit, some of the argument parsing will give problems (i.e., you can then not reliably quote an argument that contains spaces, such as an LTL formulae)

To run Spin, even from the precompiled version, you also need a C-compiler and a C-preprocessor, because Spin generates its model checking software as C-source files that require compilation before a (fast) verification can be performed. (to find public versions, see Related software).

Install all of: gcc.exe, cpp.exe, go32.exe, and spin.exe in the gcc\bin directory, which should be part of the search path you setup in the autoexec.bat file on your PC (as per the instructions from the gcc readme.1st file). In any case, do not keep spin.exe in the same directory as the Promela files you'll be working on.

Adding Xspin

To run Xspin on the PC, you need the PC version of Tcl/Tk, which you can find under Related software. (Note: Tcl/Tk does not work under Windows 3.1)

The xspin*.tcl source is contained in the .zip file of the distribution. Copy the 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. Make sure the extension .tcl is recognized as a 'wish' file by the system, so that xspin starts up when you double click the xspin*.cl script.

Another, more indirect, way to force xspin to startup is to first start `wish' from the Start Menu, under Programs, then to select the larger window that comes up (the command window), and to cd to the directory where you've stored the XSpin file. Then you can start it up by typing:


	source xspin.tcl  # or whatever else you've named this

and you should be up and running.

Be careful: don't store the executable for spin itself (spin.exe) in the same directory as the tcl/tk source for xspin -- for some reason wish does not call spin.exe correctly in that case. Place spin.exe in a directory with executables within your search path (e.g., in gcc\bin where gcc.exe also lives).

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. 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 of course. 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 however do a lot without gcc.exe. The latter is required only for verifications and for the FSM views in Xspin.

`2. Related Software`

Pointers to public domain versions of five related software packages is discussed below:

Gcc,
Cpp,
Yacc,
Tcl/Tk wish, and
Dot.

GCC

On Unix you probably have gcc, or an equivalent, installed. On the PC you minimally need three executables: gcc.exe, cpp.exe, and go32.exe, and you'll need the standard C library routines and header files. All of this should be in the following three public domain zip files (load and unzip all three files):


http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2/djdev201.zip

http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2gnu/gcc2721b.zip

http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2gnu/bnu27b.zip

Rename 'go32-v2.exe' from the gcc distribution to 'go32.exe' and make sure all executables are available in your search path. To do so, you may have to add these lines to your autoexec.bat file (type 'sysedit' at the 'run' command to edit this file).


If you install spin.exe in a directory called C:\apps\Spin

and you install all gcc files (the directories gcc\include,

gcc\bin, and gcc\lib) in a directory called C:\apps\gcc

Then, add the following lines to your AUTOEXEC.BAT file and

reboot the system:



PATH=C:\apps\Spin;C:\apps\gcc\bin

set DJGPP=C:\apps\gcc\DJGPP.ENV

In case of trouble, check the following file for details:


http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2/readme.1st

Tcl/Tk Wish

To run Xspin you'll need Tcl/Tk. Tcl/Tk was written by John Ousterhout (john.ousterhout@eng.sun.com) and is public domain. It can be obtained (for PCs or Unix) via anonymous ftp from the system ftp.smli.com in directory /pub/tcl or via URL


  	http://sunscript.sun.com/

more information can also be found in netnews-group: comp.lang.tcl

Yacc (optional)

To compile Spin itself from its sources on a PC, you'll need to have a copy of yacc installed. A public domain version for a PC can be obtained from:


	ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.Z

(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)

Dot (optional)

Dot is a graph layout tool developed by Stephen North and colleagues at AT&T (email: north@research.att.com). Xspin can make use of Dot to beautify the layout of the state-machines in the FSM-view option (highly recommended!). To obtain Dot, see


	http://www.research.att.com/sw/tools/graphviz/

The basic version of Dot is for Unix systems; there are also local ports to PCs, but it is uncertain if any of these are in the public domain. For documentation of Dot see:


	A Technique for Drawing Directed Graphs,

	by Gansner, Koutsofios, North and Vo,

	IEEE-TSE, March, 1993.

Spin HomePage (Page Updated: 16 March 1998)