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.