spin(1) [plan9 man page]

SPIN(1) 						      General Commands Manual							   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 concurrent 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.

       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 combined with -a (see below).

       v      Verbose mode: add extra detail and include more warnings.

       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 available on the target machine can still be ana-
	      lyzed 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 reduction rules take effect dur-
	      ing 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, different  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''.

																	   SPIN(1)