SPIN(1)                                                   SPIN(1)

     NAME
          spin - verification tool for concurrent systems

     SYNOPSIS
          spin [ -nN ] [ -plgrsmv ] [ -iat ] [ -DV ] [ file ]

     DESCRIPTION
          Spin is a tool for analyzing the logical consistency of con-
          current systems, specifically communication protocols.  The
          system is specified in a guarded command language called
          PROMELA2.  The language, described in the references, allows
          for the dynamic creation of processes, nondeterministic case
          selection, loops, gotos, variables, and the specification of
          correctness requirements.  The tool has fast algorithms for
          analyzing arbitrary liveness and safety conditions.

          Given a model system specified in PROMELA2, spin can perform
          interactive, guided, or random simulations of the system's
          execution or it can generate a C program that performs an
          exhaustive or approximate verification of the system.  The
          verifier can check, for instance, if user specified system
          invariants are violated during a protocol's execution, or if
          non-progress execution cycles exist.

          Without any options the program performs a random simulation
          of the system defined in the input file, default standard
          input.  The option -nN sets the random seed to the integer
          value N.

          The group of options -pglmrsv is used to set the level of
          information reported about the simulation run.  Every line
          of output normally contains a reference to the source line
          in the specification that caused it.

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

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

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

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

          s    Show all message-send events.

     SPIN(1)                                                   SPIN(1)

          m    Ordinarily, a send action will be delayed if the target
               message buffer if full.  With this option a message
               sent to a full buffer is lost.  The option can be com-
               bined with -a (see below).

          v    Verbose mode: add extra detail and include more warn-
               ings.

          i    Perform an interactive simulation.

          a    Generate a protocol-specific verifier.  The output is
               written into a set of C files, named pan.[cbhmt], that
               can be compiled (cc pan.c) to produce an executable
               verifier.  Systems that require more memory than avail-
               able on the target machine can still be analyzed by
               compiling the verifier with a bit state space:

                  cc -DBITSTATE pan.c

               This collapses the state space to 1 bit per system
               state, with minimal side-effects.  Partial order reduc-
               tion rules take effect during the verification if the
               compiler directive -DREDUCE is used.

               The compiled verifiers have their own sets of options,
               which can be seen by running them with option -?.

          t    If the verifier finds a violation of a correctness
               property, it writes an error trail.  The trail can be
               inspected in detail by invoking spin with the -t
               option.  In combination with the options pglrsv, dif-
               ferent views of the error sequence are then be
               obtained.

          D    Perform a static dataflow analysis.

          V    Print the version number and exit.

     SEE ALSO
          G.J. Holzmann, Design and Validation of Computer Protocols,
          Prentice Hall, 1991.
          -, ``Using SPIN''.