*** UNIX MANUAL PAGE BROWSER ***

SPIN(1) General Commands Manual SPIN(1) NAME spin - protocol analysis software SYNOPSIS spin [ -nN ] [ -pglprsm ] [ -at ] [ file ] DESCRIPTION Spin is a tool for analyzing the logical consistency of concurrent sys- tems, 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, nondeter- ministic 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 ran- dom simulations of the system's execution or it can generate a C pro- gram 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 simulation. With op- tion -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 spec- ification 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 num- ber. For each message parameter, show the message type and the message channel number and name. 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 reception, it writes an er- ror trail into a file named pan.trail. The trail can be in- spected in detail by invoking spin with the t option. In combi- nation with the options pglrs different views of the error se- quence are then easily obtained. SEE ALSO cospan in langs(1) G.J. Holzmann, `Spin -- A Protocol Analyzer', this manual, Volume 2. SPIN(1)