verif/Spin/README.html

   1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
   2 <!-- saved from url=(0040)http://spinroot.com/spin/Man/README.html -->
   3 <HTML><HEAD><TITLE>Spin - Version 5.1 - December 2007</TITLE>
   4 <META http-equiv=Content-Type content="text/html; charset=windows-1252">
   5 <META content="MSHTML 6.00.2800.1276" name=GENERATOR></HEAD>
   6 <BODY bgColor=#ffffff>
   7 <p>
   8 <H1><TT><FONT color=#ff0000>SPIN README</FONT></TT></H1>
   9 <ul></ul>
  10 <H2><TT>Overview of this File</TT></H2>
  11 <OL>
  12   <LI><A href="http://spinroot.com/spin/Man/README.html#S2">Downloading Spin</A>
  13   <LI><A href="http://spinroot.com/spin/Man/README.html#S1">Installing Spin</A>
  14   <LI><A href="http://spinroot.com/spin/Man/README.html#S3">Related software
  15   (gcc, cpp, tcl/tk wish, yacc, dot, jspin, ltl2ba)</A> </LI></OL>
  16 <HR>
  17
  18 <H2><TT>0. Overview</TT></H2>This readme file contains the guidelines for
  19 downloading and installing Spin and related software on Unix/Linux and Windows
  20 platforms. Refer to <A href="http://spinroot.com/spin/whatispin.html">Spin's
  21 homepage</A> for a general description of Spin, with pointers to <A
  22 href="http://spinroot.com/spin/Man/index.html">manual pages</A>, <A
  23 href="http://spinroot.com/spin/News/index.html">newsletters</A>.
  24 <p>Spin is distributed in source form to encourage research in formal
  25 verification, and to help a support friendly and open exchange of algorithms,
  26 ideas, and tools. The software itself has a copyright from Lucent Technologies
  27 and Bell Laboratories, and is distributed for research and educational purposes
  28 only (i.e., no guarantee of any kind is implied by the distribution of the code,
  29 and all rights are reserved by the copyright holder). For this general use of
  30 Spin, no license is required.
  31 <p>Commercial application of the Spin software is also allowed, but requires the
  32 acceptance of a basic license. Refer to the <A
  33 href="http://www.spinroot.com/spin/spin_license.html">Spin Public license</A> for details.
  34 <p>
  35 <HR>
  36
  37 <H2><TT><A name=S2>1. Downloading Spin</A></TT></H2>Spin runs on Unix,
  38 Solaris, and Linux machines, on most flavors of Windows PCs, and on Macs.
  39 Precompiled binary executables for some popular types of machines are available
  40 in the
  41 <A href="http://spinroot.com/spin/Bin/index.html">Spin Binaries</A>.
  42 <p>
  43 All binaries have an extension that matches the Spin version number,
  44 such as <tt>spin427.exe</tt>. To install the binary, rename it to
  45 <tt>spin.exe</tt> and copy it into your bin directory.
  46 <p>
  47 If you have machine type that is not available there, or if you are
  48 installing Spin for the first time, then follow the more detailed instructions
  49 below.
  50 <ul>
  51   <LI><B>Unix</B> systems: <BR>download the most recent .tar-file with sources,
  52   the graphical interface Xspin, documentation and examples from the <A
  53   href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>, and
  54   continue at <A href="http://spinroot.com/spin/Man/README.html#S1a"><FONT
  55   color=red><B><TT>Step 2a</TT></B></FONT></A>.</LI>
  56   <p></p>
  57   <LI><B>PCs</B> (Windows95/98/2000/NT/XP): <BR>download the most recent
  58   pc_spin*.zip file, with a precompiled Spin executable, the graphical interface
  59   Xspin, and some examples from the <A
  60   href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>, and
  61   continue at <A href="http://spinroot.com/spin/Man/README.html#S1b"><FONT
  62   color=red><B><TT>Step 2b</TT></B></FONT></A>. </LI>
  63   <p></p>
  64   <LI><B>Macs</B> (Mac OS X): <BR>download the most recent .tar-file with sources,
  65   from the <A href="http://spinroot.com/spin/Src/index.html">Spin Distribution</A>,
  66   and continue at <A href="http://spinroot.com/spin/Man/README.html#S1c"><FONT
  67   color=red><B><TT>Step 2c</TT></B></FONT></A>.
  68   </LI></ul>
  69 <p>
  70 <HR>
  71
  72 <H2><TT><A name=S1>2. Installing Spin</A></TT></H2>
  73 <ul>
  74   <LI><A href="http://spinroot.com/spin/Man/README.html#S1a"><TT>Unix/Linux
  75   systems</TT> (compiled from the sources)</A>
  76   <LI><A href="http://spinroot.com/spin/Man/README.html#S1b"><TT>Windows
  77   PC's</TT> (using the executable)</A> </LI>
  78   <LI><A href="http://spinroot.com/spin/Man/README.html#S1c"><TT>Macs
  79   </TT> (compiled from the sources, with some patches)</A> </LI></ul><p>
  80 <HR>
  81
  82 <H2><TT><A name=S1a><FONT color=red>2a. Installing Spin on a Unix/Linux
  83 System</A></FONT></TT></H2>
  84 <ul>Place the *.tar.gz file from the <A
  85   href="http://spinroot.com/spin/Src/index.html">Spin Source Distribution</A> in
  86   clean directory, and cd to that directory. If you have a standard Unix/Linux system,
  87   unpack the archive, and compile an executable, for instance as follows: <pre> gunzip *.tar.gz
  88         tar -xf *.tar
  89         cd Src*
  90         make    # or, on older distributions: make -f make_unix
  91 </pre>
  92   <p>If you are on a SOLARIS system, edit the makefile and add
  93   <TT>-DSOLARIS</TT> to the compiler directives in the makefile before you type
  94   'make'. Similarly, if you use a different C compiler than defined in the
  95   makefile, edit the makefile first. You need to have at least a C compiler and
  96   a copy of yacc.
  97   <p>If all else fails, you can also compile everything with the following line:
  98 <pre>   yacc -v -d spin.y; cc -o spin *.c
  99 </pre>
 100   <p>Spin should compile without warnings. Install the executable version of
 101   spin in a directory that is within your default search path (such as your home
 102   bin directory, or /usr/local/bin etc.)
 103   <p>
 104   On Unix/Linux systems Spin assumes that the standard C preprocessor cpp is
 105   stored in file "/lib/cpp". On some systems this is different: check the
 106   comments in the makefile for details if you run into this problem.
 107
 108   <H3><TT>Testing</TT></H3>To test the basic sanity of the Spin executable, cd
 109   to the Test directory that was created when you unpacked the source archive,
 110   and follow the instructions in README.tests file that is included there.
 111   <H3><TT>Adding Xspin (Unix/Linux)</TT></H3>Xspin is an optional, but highly
 112   recommended, graphical user interface to Spin, written in Tcl/Tk. To obtain
 113   Tcl/Tk, see <A href="http://spinroot.com/spin/Man/README.html#S3">Related
 114   software</A>. The Xspin source can be found the Xspin4.? directory that will
 115   also have been created when you unpacked the source tarfile.
 116   <p>The current version of Xspin is compatible with
 117 <pre>   Tk version 4.2 - Tcl version 7.6
 118         Tk version 8.4 - Tcl version 8.4
 119 </pre>
 120   <p>Xspin prints the version numbers of Spin, Xspin, and Tcl/Tk when it starts
 121   up. You can also check separately which version of Tcl/Tk you have installed
 122   by executing the following commands in `wish' (a Tcl/Tk command): <pre>       info tclversion
 123         puts $tk_version
 124 </pre>You can find out which version of Spin you have by typing, at the
 125   command prompt: <pre> $ spin -V
 126 </pre>
 127   <p>Xspin can also make use the graph layout program 'dot' if it is available
 128   on your system (not required, but very nice if available -- xspin will
 129   automatically recognize if it is installed.) For information on 'dot,' see <A
 130   href="http://spinroot.com/spin/Man/README.html#S3">Related software</A>.
 131   <p>To install Xspin on Unix/Linux:
 132   <ul>
 133     <LI>cd to directory Xspin... from the distribution,
 134     <LI>Rename xspin*.tcl into a more convenient form (like xspin or xspin.tcl)
 135     and follow the instructions at the top of this xspin.tcl file. Minimally:
 136     you must change the first few lines of this file to point to the executable
 137     `wish' command on your system that you want to use. If you use another
 138     C-compiler than the default (gcc), you should update the global variable CC
 139     inside xspin as well. Follow the instructions inside the xspin.tcl file to
 140     do so.
 141     <LI>copy the file into a directory within your search path, renamed to plain <tt>xspin</tt>
 142 and make it
 143     executable, for instance:
 144 <pre>   cp xspin510.tcl /usr/local/bin/xspin
 145         chmod +x /usr/local/bin/xspin
 146 </pre>
 147     <LI>On Unix/Linux, invoke the program by typing
 148 <pre>   xspin   # or xspin.tcl if you keep the extension...
 149 or
 150         xspin promela_spec
 151
 152 For example:
 153         cd Test
 154         xspin leader
 155 </pre></LI></ul>Check the online Help menus in xspin for more details on
 156   routine use. </ul>
 157 <p>
 158 <HR>
 159
 160 <H2><TT><A name=S1b><FONT color=red>2b. Installing Spin on a Windows
 161 PC</FONT></A></TT></H2>
 162 <ul>If you just need to update the Spin executable itself, download a new
 163   version from <A
 164   href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>
 165   If you need more files, e.g. a new copy of Xspin, download the latest
 166   pc_spin*.zip file from <A
 167   href="http://spinroot.com/spin/Src/index.html">http://spinroot.com/spin/Src/index.html</A>
 168   Extract the files from pc_spin*.zip, and copy spin*.exe, renamed spin.exe, into the directory
 169   where all your commands reside and that is within your default search path
 170   (e.g., c:/cygwin/bin/, or c:\apps\spin\) You can find out what your search
 171   path is set to by typing 'set' at an MS-DOS prompt -- this prints a list of
 172   all defined variables in your environment, including the search path that is
 173   used to find executable commands.
 174   (Note that you may need to set the search path in the environment variables)
 175   <p>If you use Spin from the command line (i.e., without Xspin), be warned that
 176   some command shells, e.g., the MKS Korn-shell, have none-standard rules for
 177   argument parsing (i.e., you can not reliably quote an argument that contains
 178   spaces, such as an LTL formula). In most cases this will not be much of a
 179   problem, except with the conversion of LTL formula with the Spin -f option.
 180   You can circumvent this by using -F instead of -f, to read the formula from a
 181   file instead of the command line.
 182   <p>To run Spin, also with the precompiled version, you need a working
 183   C-compiler and a C-preprocessor, because Spin generates its model checking
 184   software as C-source files that require compilation before a verification can
 185   be performed. This guarantees fast model checking, because each model checker
 186   can be optimized to the specific model being checked. Check, for instance, if
 187   you can compile and run a minimal C program succesfully, e.g.:
 188 <pre>
 189         #include &#60;stdio.h&#62;
 190         int main(void) { printf("hello\n"); }
 191 </pre>
 192   <p>To find a public version of a C compiler and some instructions on how to
 193   install it see <A href="http://spinroot.com/spin/Man/README.html#S3">Related
 194   software</A>.
 195   <H3><TT>Adding Xspin (PC)</TT></H3>To run Xspin on a PC, you need the PC
 196   version of Tcl/Tk, which you can find under <A
 197   href="http://spinroot.com/spin/Man/README.html#S3">Related software</A>.
 198   <p>The xspin*.tcl source is contained in the .zip file of the <A
 199   href="http://spinroot.com/spin/Src/index.html">distribution</A>. Copy the .tcl
 200   file as is into a directory where you plan to work, or put a shortcut to this
 201   file on the Desktop or in the Start Menu. If you keep the extension .tcl, make
 202   sure it is recognized as a 'wish' file by the system, so that xspin starts
 203   when you double click the xspin*.tcl script.
 204   <p>Under cygwin, copy the xspin*.tcl file to /bin/xspin and make it executable
 205   -- check the first few lines of xspin*.tcl to make sure the location of xspin
 206   matches what you have on your system (it is currently setup for
 207   c:/cygwin/bin/xspin). You can now use xspin as a normal Unix-style command,
 208   and you can pass the name of a filename to it, for instance as: <pre> xspin leader
 209 </pre>
 210   <p>An indirect way to force xspin to startup is to first start `wish' from the
 211   Start Menu, under Programs, then select the larger window that comes up (the
 212   command window), and cd to the directory where you've stored the xspin.tcl
 213   file. Then you can then start it up by typing: <pre>  source xspin.tcl  # or whatever else you've named this
 214 </pre>and you should be up and running.
 215   <p>The PC installation assumes that you have a command called "cpp.exe"
 216   available (which comes with the gnu-c installation), which is the traditional
 217   name of the C preprocessor. Alternatively, it can also use the Visual C++
 218   compiler, which is named cl.exe for preprocessing. To complicate your life
 219   somewhat, if you have a copy of the Borland C++ compiler installed, you'll
 220   notice that this cplusplus compiler was also named cpp.exe -- that's not the
 221   cpp you want. To avoid the name clash, you either have to edit the Spin source
 222   code to give it the full path name of the 'real' cpp.exe and recompile, or use
 223   Spin with the command-line option -Pxxxx where xxxx is the path for cpp.exe.
 224   Nothing much in Spin will work without access to cpp.exe. You can do a
 225   reasonable number of things without gcc.exe though (like simulations). The
 226   C-compiler is required for all verifications and for the automata views in
 227   Xspin. </p></ul>
 228 <p>
 229 <H2><TT><A name=S1c><FONT color=red>2c. Installing Spin on a Mac</FONT></A></TT></H2>
 230   <ul>
 231   Compile Spin from its sources, as described under 2a for Unix systems in general,
 232   while following the suggestions below, which were provided by
 233   Dominik Brettnacher, email: <tt>domi@saargate.de</tt>.
 234 <p>
 235 The C preprocessor on Mac OS X cannot be found in <tt>/lib</tt>.
 236 Change the path in the makefile for the
 237 proper location (<tt>/usr/bin/cpp</tt>), and in addition
 238 also tell the Mac preprocessor to handle its input as
 239 "assembler-with-cpp."
 240 This can be done by adding a flag to cpp, for instance in
 241 the makefile by adding the directive
 242 <ul>
 243 <pre>
 244 -DCPP="\"/usr/bin/cpp -xassembler-with-cpp\""
 245 </pre>
 246 </ul>
 247 to the definition of <tt>CFLAGS</tt>.
 248 </pre>
 249 <p>
 250 <H3><TT>Adding Xspin (Unix)</TT></H3>
 251 On the Mac, Xspin is known to work correctly with Tcl/Tk Aqua,
 252 which offers a self-contained binary distribution for the Mac.
 253 Use, for instance, "TclTkAquaStandalone", version 8.4.4 from
 254 <ul>
 255 <pre><a href="http://www.maths.mq.edu.au/~steffen/tcltk/TclTkAqua/">http://www.maths.mq.edu.au/~steffen/tcltk/TclTkAqua/</a>
 256 </pre>
 257 </ul>
 258 <p>
 259 Xspin by default places its temporary files into the root directory.
 260 This is nasty if you have admin privileges and probably leads to error
 261 messages if you don't.
 262 To prevent this, add a "cd" statement to xspin (no arguments, just cd by
 263 itself on a line), as the first command executed.
 264 Place it, for instance, directly after the opening comments in the file.
 265 This makes Xspin use the home directory for these files.
 266 <p>
 267 TclTk Aqua also provides the possibility to start a script when being run.
 268 For instance, to make Xspin start if you launch the TCL interpreter:
 269 move the xspin file into the "Wish Shell.app", as follows:
 270 <ul><pre>
 271 chmod -R u+w Wish\ Shell.app
 272 mkdir Wish\ Shell.app/Contents/Resources/Scripts
 273 mv xspin*.tcl Wish\ Shell.app/Contents/Resources/Scripts/AppMain.tcl
 274 </pre>
 275 </ul>
 276 </ul>
 277
 278 <HR>
 279
 280 <H2><TT><A name=S3>3. Related Software</A></TT></H2>
 281 <ul>Pointers to public domain versions of some related software packages are
 282   discussed below:
 283   <ul>
 284     <LI>Gcc,</LI>
 285     <LI>Cpp,</LI>
 286     <LI>Yacc,</LI>
 287     <LI>Tcl/Tk wish,</LI>
 288     <LI>Dot,</LI>
 289     <LI>JSpin, and</LI>
 290     <LI>Ltl2Ba. </LI></ul>
 291   <H3><TT>GCC</TT></H3>On Unix/Linux you probably have gcc, or an equivalent,
 292   installed. On the PC you need either a copy of Visual Studio Express (for the cl
 293   command), or an installation of gcc with minimally the executables: gcc.exe,
 294   and cpp.exe in your search path, together with all the standard C library
 295   routines and header files. You can get good free version of all these files
 296   with the <TT>cygwin</TT> toolkit, which is mostly self-installing and
 297   available from: <A href="http://www.cygwin.com/">http://www.cygwin.com/</A>
 298   <BR>See also what's available in <A
 299   href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>.
 300
 301   <H3><TT>Tcl/Tk Wish</TT></H3>To run Xspin you'll need Tcl/Tk. Tcl/Tk was
 302   written by John Ousterhout (john.ousterhout@eng.sun.com) and is public domain.
 303   It can be obtained (for PCs or Unix) from cygwin, or from: <A
 304   href="http://www.tcl.tk/">http://www.tcl.tk/</A> or also (a more recent extension):
 305   <a href="http://www.activestate.com/Products/ActiveTcl/">
 306   http://www.activestate.com/Products/ActiveTcl/</a><BR>More details can be found
 307   in netnews-group: comp.lang.tcl
 308
 309   <H3><TT>Yacc (optional)</TT></H3>To compile Spin itself from its sources on a
 310   PC, you'll need to have a copy of yacc installed. A public domain version for
 311   a PC can most easily be obtained from <b>cygwin</b>, or also from:
 312 <pre>   <A href="ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.Z">ftp://ftp.cs.berkeley.edu/ucb/4bsd/byacc.tar.Z</A>
 313 </pre>A copy of this file is also available in: <A
 314   href="http://spinroot.com/spin/Bin/index.html">http://spinroot.com/spin/Bin/index.html</A>
 315   (You don't need yacc on the PC's if you use the pre-compiled version of Spin
 316   for the pc in the pc*.zip file from the distribution) Look at the file
 317   make_it.bat for an example on how to perform the compilation.
 318   <H3><TT>Dot (optional)</TT></H3>Dot is a graph layout tool developed by
 319   Stephen North and colleagues at AT&amp;T (email: north@research.att.com).
 320   Xspin can make use of dot to beautify the layout of the state-machines in the
 321   automata-view option (recommended!).
 322 To obtain Dot, see
 323 <pre>
 324         <A href="http://www.graphviz.org/">http://www.graphviz.org/</A>
 325 </pre>
 326 The are both PC and Unix versions of dot available. For documentation of
 327 dot see, for instance:
 328 <pre><I>        A technique for drawing directed graphs</I>,
 329         by Gansner, Koutsofios, North and Vo,
 330         IEEE-TSE, March, 1993.
 331 </pre>
 332 If you accept the default installation on a PC, you will need to define the
 333 location of dot.exe in the xspin source as follows:
 334 <pre>
 335         set DOT "C:/Program\\ Files\ATT\Graphviz/bin/dot.exe"
 336 </pre>
 337 (the line that sets the location of DOT appears near the top of the xspin.tcl file).
 338 <H3><TT>JSpin (optional)</TT></H3>
 339 An alternative to the Xspin GUI, written in Java instead of Tcl/Tk.
 340 Written by Moti Ben-Ari (moti.ben-ari@weizmann.ac.il), see
 341 <pre>
 342         <a href="http://stwww.weizmann.ac.il/g-cs/benari/jspin/">http://stwww.weizmann.ac.il/g-cs/benari/jspin/</a>
 343 </pre>
 344 The jSpin tool currently expects spin to be installed on Windows in c:/spin/spin.exe, and it assumes that you are using the
 345 mingw version of gcc.
 346   <H3><TT>Ltl2Ba (optional)</TT></H3>A faster method to generate very small
 347   never claims from LTL formulae, developed by Denis Oddoux and Paul Gastin is
 348   available online in source form:
 349 <pre>
 350         <A href="http://spinroot.com/spin/Src/ltl2ba.tar.gz">http://spinroot.com/spin/Src/ltl2ba.tar.gz</A>
 351 </pre>
 352 The latest version can be obtained from the authors website via:
 353 <pre>
 354         <A href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php">http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php</A>
 355 See also
 356         <A href="http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php">http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php</A>
 357 </pre>
 358 The C source code can be linked with Spin, or run as a standalone tool.
 359 <p>
 360 </ul>
 361 <HR>
 362 <TT>
 363 <TABLE cols=3 width="100%">
 364 <TBODY><TR>
 365 <TD align=left><A href="http://spinroot.com/spin/whatispin.html"><TT>Spin HomePage</TT></A></TD>
 366 <TD></TD>
 367 <TD align=right><FONT size=3><B><TT>
 368 (Page Last Updated: 26 April 2008)
 369 </TT></B></FONT></TD>
 370 </TR></TBODY>
 371 </TABLE>
 372 </TT>
 373 </BODY>
 374 </HTML>