SPIN(1)                                                   SPIN(1)

     NAME
          spin - verification tool for models of concurrent systems

     SYNOPSIS
          spin -a [ -m ] [ -Pcpp ] file

          spin [ -bglmprsv ] [ -nN ] [ -Pcpp ] file

          spin -c [ -t ] [ -Pcpp ] file

          spin -d [ -Pcpp ] file

          spin -f ltl

          spin -F file

          spin -i [ -bglmprsv ] [ -nN ] [ -Pcpp ] file

          spin -M [ -t ] [ -Pcpp ] file

          spin -t[N] [ -bglmprsv ] [ -jN ] [ -Pcpp ] file

          spin -V

     DESCRIPTION
          Spin is a tool for analyzing the logical consistency of
          asynchronous systems, specifically distributed software and
          communication protocols.  A verification model of the system
          is first specified in a guarded command language called
          Promela. This specification language, described in the ref-
          erence, allows for the modeling of dynamic creation of asyn-
          chronous processes, nondeterministic 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 or approximate verification of the correctness
          requirements for the system.

          -a   Generate a verifier (model checker) for the specifica-
               tion.  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 manu-
               als (see below) contain the details on compilation and
               use of the verifiers.

     SPIN(1)                                                   SPIN(1)

          -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.

          -d   Produce symbol table information for the model speci-
               fied in file. For each Promela object this information
               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 (glo-
               bal or local), and whether the object is declared as a
               variable or as a parameter.  For message 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 vari-
               able.

          -f ltl
               Translate the LTL formula ltl into a never claim.
               This option reads a formula in LTL syntax from the sec-
               ond 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 compatibility with
               the partial order reduction rules that are applied dur-
               ing the verification process.  If the formula contains
               spaces, it should be quoted to form a single argument
               to the spin command.

          -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 annotation on the for-
               mula.  (On some systems the quoting conventions of the
               shell complicate the use of option -f.  Option -F is
               meant to solve those problems.)

          -i   Perform an interactive simulation, prompting the user
               at every execution step that requires a nondeterminis-
               tic choice to be made.  The simulation proceeds without
               user intervention when execution is deterministic.

          -M   Produce a message sequence chart in Postscript form for
               a random simulation or a guided simulation (when com-
               bined 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

     SPIN(1)                                                   SPIN(1)

               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 inte-
               ger N.

          -t   Perform a guided simulation, following the error trail
               that was produces by an earlier verification run, see
               the online manuals for the details on verification.

          -V   Prints the spin version number and exits.

          With only a filename as an argument and no options, spin
          performs a random simulation of the model specified in the
          file (standard input is the default if the filename is omit-
          ted).  If option -i is added, the simulation is interactive,
          or if option -t is added, the simulation is guided.

          The simulation 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 -bglmprsv sets the desired level of infor-
          mation that the user wants about a random, guided, or inter-
          active simulation run.  Every line of output normally con-
          tains a reference to the source line in the specification
          that generated it.

          -b   Suppress the execution of printf statements within the
               model.

          -g   Show at each time step the current value of global
               variables.

          -l   In combination with option -p, show the current value
               of local variables of the process.

          -p   Show at each simulation step which process changed
               state, and what source statement was executed.

          -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   Show all message-send events.

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

     SPIN(1)                                                   SPIN(1)

     SOURCE
          /sys/src/cmd/spin

     SEE ALSO
          http://spinroot.com: GettingStarted.pdf, Roadmap.pdf,
              Manual.pdf, WhatsNew.pdf, Exercises.pdf
          G.J. Holzmann, Design and Validation of Computer Protocols,
          Prentice Hall, 1991.
          , `Design and validation of protocols: a tutorial,'
          Computer Networks and ISDN Systems, Vol. 25, No. 9, 1993,
          pp. 981-1017.
          , `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No.
          5, May 1997.