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.
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.
If you already have a version 3 of Spin installed, you may prefer to use a shell script to update the sources to the most recent version:
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 *.cSpin 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, 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_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, cd to directory Xspin3.3 from the distribution,
cp xspin.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 leaderCheck the online Help menus in xspin for more details on routine use.
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.
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 thisand 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 ""
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.zipOr 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:
Rename 'go32-v2.exe' from the distribution (in the \gcc\bin directory) to 'go32.exe', as per the instructions from the gcc readme.1st file.
Once you've compiled spin.exe, also add spin.exe to \apps\gcc\bin, or anywhere else that will be within your search path. In any case, do not keep spin.exe in the same directory as the Promela files you'll be working on.
Next, make sure all executables are available in your search path. To do so on a Windows95/98 system: edit the AUTOEXEC.BAT by selecting 'Run' from the Start Menu, and type 'sysedit'. Select the AUTOEXEC.BAT file and add the following two lines:
PATH=C:\apps\gcc\bin set DJGPP=C:\apps\gcc\DJGPP.ENVThen reboot your system.
To add the right settings on a WindowsNT system, from the Start Menu select 'Control Panel,' select 'System,' and then select 'Environment.' Add C:\apps\gcc\bin to an existing PATH definition, or add a new variable with this value. Similarly, add a variable DJGPP to your environment and give it the value: C:\apps\gcc\DJGPP.ENV Then reboot your system.
Make sure that the file C:\apps\gcc\DJGPP.ENV exists on your system, and was not put somewhere else (such as C:\apps\Djdev201\djgpp.env) during the installation of the GCC distribution. Similarly, make sure that the GCC binary is really named \apps\gcc\bin, etc. If not, simply adjust the two lines above, to point to the right places.
In case of trouble, check the following file for more details:
http://www.simtel.net/pub/simtelnet/gnu/djgpp/v2/readme.1st
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
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)
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) |