man(1) Manual page archive


     SPIN(1)                                                   SPIN(1)

     NAME
          spin - protocol analysis software

     SYNOPSIS
          spin [ -nN ] [ -pglprsm ] [ -at ] [ 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
          Promela.  The language, described in the reference, allows
          for the dynamic creation of processes, nondeterministic case
          selection, loops, gotos, variables and assertions.  The tool
          has fast and frugal algorithms for analyzing liveness and
          safeness conditions.

          Given a model system specified in Promela, spin can either
          perform random simulations of the system's execution or it
          can generate a C program that performs a fast exhaustive
          validation of the system state space.  The validator can
          check, for instance, if user specified system invariants may
          be violated during a protocol's execution, or if any non-
          progress execution cycles exist.

          Without any options the program performs a random simula-
          tion.  With option

          -nN  the seed for the simulation is set explicitly to the
               integer value N.

          The second group of options -pglrs is used to set the
          desired level of information that the user wants 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.

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

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

          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.

     SPIN(1)                                                   SPIN(1)

          s    Show all message-send events.

          m    Changes the semantics of send events.  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 combined with
               -a (see below).

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

               cc -DBITSTATE pan.c

               This collapses the state space to 1 bit per system
               state, with minimal side-effects.

               A compiled analyzer has its own set of options, which
               can be seen by typing a.out -?.

          t    If the analyzer finds a violation of an assertion, a
               deadlock, a non-progress loop, or an unspecified recep-
               tion, it writes an error trail into a file named
               pan.trail.  The trail can be inspected in detail by
               invoking spin with the t option.  In combination with
               the options pglrs different views of the error sequence
               are then easily obtained.

     SEE ALSO
          cospan in langs(1)
          G.J. Holzmann, `Spin - A Protocol Analyzer', this manual,
          Volume 2.