Spin - Version 3.3 - September 1999

SPIN README

Overview of this File

  1. Downloading Spin
  2. Installing Spin
  3. Related software (gcc, cpp, go32, wish, dot)
This readme file contains the guidelines for downloading and installing Spin and related software on Unix and Windows platforms. Refer to Spin's homepage for a general description of Spin, with pointers to manual pages, newsletters.

Spin is distributed in source form to encourage 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 the code, and all rights are reserved by the copyright holder). For educational or research use of Spin, no license is required. Commercial applications require a standard limited-use license which carries a small administrative fee. Please send email for details if you need such a license.

1. Downloading Spin

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. See below for more specific directions.

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

1a. Installing Spin on a Unix System

By default:

If you are on a SOLARIS system, add -DSOLARIS to the compiler directives in the makefile first. (On a PC you need to add -DPC, but you're better off using the precompiled version in this case; see below.) 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)

Type 'make'

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 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: check the comments in the makefile for details if you run into this problem.

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 user interface to Spin, written in Tcl/Tk. To obtain Tcl/Tk, see Related software below. The Xspin source can be found the Xspin3.3 directory.

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
(Be warned: It does not (yet) work with Tcl/Tk version 8.1.)

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

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, cd to directory Xspin3.3 from the distribution,

  1. Rename xspin333.tcl into a more convenient form (like xspin or xspin.tcl) and follow the instructions at the top of this xspin.tcl file. Minimally: you must 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.tcl file to do so.
  2. copy the file into a directory within your search path and make it executable, for instance:
    	cp xspin.tcl /usr/local/bin/xspin
    	chmod +x /usr/local/bin/xspin
    
  3. 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.tcl if you keep the extension...
or
	xspin promela_spec

For example:
	cd Test
	xspin leader
Check the online Help menus in xspin for more details on routine use.

1b. Installing Spin on a Windows95/98 or WindowsNT PC

Unzip the compressed file pc*.zip, and copy spin.exe into a directory with executables that is in your search path. (You can find out what your search path is set to by typing 'set' at an MS-DOS prompt -- this prints a list of all defined variables in your environment, including the search path that is used to find executable commands.)

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

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 verification can be performed. This guarantees fast model checking, because each model checker can be optimized to the specific model being checked.

It is recommended to put spin.exe in the same bin directory that you use to store the C-compiler, e.g., \apps\gcc\bin (as explained under Related software).

To find a public version of a C compiler and some instructions on how to install it see Related software.

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 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 start it up by typing:

	source xspin.tcl  # or whatever else you've named this
and you should be up and running.

Don't store the executable for spin itself (spin.exe) in the same directory as the tcl/tk source for xspin -- for some reason some versions of wish do not call spin.exe correctly in that case. Place spin.exe in a directory with executables within your search path (e.g., in c:\apps\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 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.

By default, the PC version of xspin tries to run compiled programs with the 32-bit extender 'go32.exe' that comes with the gcc distribution. If for some reason this fails (xspin will say 'could not run verification' when you try to do so) edit the xspin*.tcl file -- find the line that says:

	set GO32 "go32"
and replace it with:
	set GO32 ""

2. Related Software

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

GCC

On Unix you probably have gcc, or an equivalent, installed. On the PC you need two or three executables: gcc.exe, cpp.exe, and sometimes also go32.exe, plus the standard C library routines and header files installed. 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
Or if the last two are no longer available, try the newer versions:
http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2gnu/gcc2721b.zip
http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2gnu/bnu27b.zip

Some users (especially on Windows NT systems) prefer to use
the cygwin package, that is mostly self-installing
and available from:

http://sourceware.cygnus.com/cygwin

If you use the gnu software from simtel, proceed as follows:

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 via URLs
	ftp://ftp.scriptics.com/pub/tcl/tcl8_0/tcl80p2.exe

or via:

  	http://www.scriptics.com/

More details can be found at http://www.scriptics.com/ and 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 automata-view option (recommended!). To obtain Dot, see
	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.


Spin HomePage (Page Updated: 9 September 1999)