man(1) Manual page archive


     SPIN(1)                                                   SPIN(1)

     NAME
          spin - verification tool for models of concurrent systems

     SYNOPSIS
          spin [ options ] file
          spin -V

     DESCRIPTION
          Spin is a tool for analyzing the logical consistency of
          asynchronous systems, specifically distributed software,
          multi-threaded systems, and communication protocols.  A
          model of the system is specified in a guarded command lan-
          guage called Promela (process meta language).  This modeling
          language supports dynamic creation of processes, nondeter-
          ministic case selection, loops, gotos, local and global
          variables.  It also allows for a concise specification of
          logical correctness requirements, including, but not
          restricted to requirements expressed in linear temporal
          logic.

          Given a Promela model stored in file, spin can perform
          interactive, guided, or random simulations of the system's
          execution.  It can also generate a C program that performs
          an exhaustive verification of the correctness requirements
          for the system.  The main options supported are as follows.
          (You can always get a full list of current options with the
          command "spin --").

          -a     Generate a verifier (a model checker) for the speci-
                 fication.  The output is written into a set of C
                 files named pan.[cbhmt], that can be compiled (pcc
                 pan.c) to produce an executable verifier.  The online
                 spin manuals contain the details on compilation and
                 use of the verifiers.

          -b     Do not execute printf statements in a simulation run.

          -c     Produce an ASCII approximation of a message sequence
                 chart for a random or guided (when combined with -t)
                 simulation run. See also option -M.

          -Dxxx  Pass -Dxxx to the preprocessor (see also -E and -I).

          -d     Produce symbol table information for the model speci-
                 fied in file. For each Promela object this informa-
                 tion includes the type, name and number of elements
                 (if declared as an array), the initial value (if a
                 data object) or size (if a message channel), the
                 scope (global or local), and whether the object is

     SPIN(1)                                                   SPIN(1)

                 declared as a variable or as a parameter.  For mes-
                 sage channels, the data types of the message fields
                 are listed.  For structure variables, the third field
                 defines the name of the structure declaration that
                 contains the variable.

          -Exxx  Pass xxx to the preprocessor (see also -D and -I).

          -e     If the specification contains multiple never claims,
                 or ltl properties, compute the synchronous product of
                 all claims and write the result to the standard out-
                 put.

          -f ltl Translate the LTL formula ltl into a never claim.
                 This option reads a formula in LTL syntax from the
                 second argument and translates it into Promela syntax
                 (a never claim, which is Promela's equivalent of a
                 Büchi Automaton).  The LTL operators are written: []
                 (always), <> (eventually), and U (strong until).
                 There is no X (next) operator, to secure compatibil-
                 ity with the partial order reduction rules that are
                 applied during the verification process.  If the for-
                 mula contains spaces, it should be quoted to form a
                 single argument to the spin command.
                 This option has largely been replaced with the sup-
                 port for inline specification of ltl formula, in Spin
                 version 6.0.

          -F file
                 Translate the LTL formula stored in file into a never
                 claim.
                 This behaves identically to option -f but will read
                 the formula from the file instead of from the command
                 line.  The file should contain the formula as the
                 first line.  Any text that follows this first line is
                 ignored, so it can be used to store comments or anno-
                 tation on the formula.  (On some systems the quoting
                 conventions of the shell complicate the use of option
                 -f.  Option -F is meant to solve those problems.)

          -g     In combination with option -p, print all global vari-
                 able updates in a simulation run.

          -h     At the end of a simulation run, print the value of
                 the seed that was used for the random number genera-
                 tor.  By specifying the same seed with the -n option,
                 the exact run can be repeated later.

          -I     Show the result of inlining and preprocessing.

          -i     Perform an interactive simulation, prompting the user
                 at every execution step that requires a

     SPIN(1)                                                   SPIN(1)

                 nondeterministic choice to be made.  The simulation
                 proceeds without user intervention when execution is
                 deterministic.

          -jN    Skip printing for the first N steps in a simulation
                 run.

          -J     Reverse the evaluation order for nested unless state-
                 ments, e.g., to match the way in which Java handles
                 exceptions.

          -k file
                 Use the file name file as the trail-file, see also
                 -t.

          -l     In combination with option -p, include all local
                 variable updates in the output of a simulation run.

          -M     Produce a message sequence chart in Postscript form
                 for a random simulation or a guided simulation (when
                 combined with -t), for the model in file, and write
                 the result into file.ps. See also option -c.

          -m     Changes the semantics of send events.  Ordinarily, a
                 send action will be (blocked) if the target message
                 buffer is full.  With this option a message sent to a
                 full buffer is lost.

          -nN    Set the seed for a random simulation to the integer
                 value N. There is no space between the -n and the
                 integer N.

          -N file
                 Use the never claim stored in file to generate the
                 verified (see -a).

          -O     Use the original scope rules from pre-Spin version 6.

          -o[123]
                 Turn off data-flow optimization ( -o1). Do not hide
                 write-only variables ( -o2 ) during verification.
                 Turn off statement merging ( -o3 ) during verifica-
                 tion.  Turn on rendezvous optimization ( -o4 ) during
                 verification.  Turn on case caching ( -o5 ) to reduce
                 the size of pan.m, but losing accuracy in reachabil-
                 ity reports.

          -O     Use the scope rules pre-version 6.0. In this case
                 there are only two possible levels of scope for all
                 data declarations: global, or proctype local.  In
                 version 6.0 and later there is a third level of
                 scope: inlines or blocks.

     SPIN(1)                                                   SPIN(1)

          -Pxxx  Use the command xxx for preprocessing instead of the
                 standard C preprocessor.

          -p     Include all statement executions in the output of
                 simulation runs.

          -qN    Suppress the output generated for channel N during
                 simulation runs.

          -r     Show all message-receive events, giving the name and
                 number of the receiving process and the corresponding
                 the source line number.  For each message parameter,
                 show the message type and the message channel number
                 and name.

          -s     Include all send operations in the output of simula-
                 tion runs.

          -T     Do not automatically indent the printf output of pro-
                 cess i with i tabs.

          -t[N]  Perform a guided simulation, following the [Nth]
                 error trail that was produces by an earlier verifica-
                 tion run, see the online manuals for the details on
                 verification. By default the error trail is looked
                 for in a file with the same basename as the model,
                 and with extension .trail.  See also -k.

          -v     Verbose mode, add some more detail, and generate more
                 hints and warnings about the model.

          -V     Prints the spin version number and exit.

          With only a filename as an argument and no option flags,
          spin performs a random simulation of the model specified in
          the file.  This normally does not generate output, except
          what is generated explicitly by the user within the model
          with printf statements, and some details about the final
          state that is reached after the simulation completes.  The
          group of options -bgilmprstv is used to set the desired
          level of information that the user wants about a random,
          guided, or interactive simulation run.  Every line of output
          normally contains a reference to the source line in the
          specification that generated it.  If option -i is included,
          the simulation i interactive, or if option -t or -kfile is
          added, the simulation is guided.

     SOURCE
          /sys/src/cmd/spin

     SEE ALSO
          http://spinroot.com/spin/Man/

     SPIN(1)                                                   SPIN(1)

          G.J. Holzmann, The Spin Model Checker (Primer and Reference
          Manual), .}f Addison-Wesley, Reading, Mass., 2004.
          , `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No.
          5, May 1997.
          , `Design and validation of protocols: a tutorial,'
          Computer Networks and ISDN Systems, Vol. 25, No. 9, 1993,
          pp. 981-1017.
          , Design and Validation of Computer Protocols, Prentice
          Hall, Englewood Cliffs, NJ, 1991.