V10/vol2/spin/spin.1

.TH SPIN 1
.CT 1 comm_mach protocol
.SH NAME
spin \(mi protocol analysis software
.SH SYNOPSIS
.B spin
[
.BI -n N
]
[
.BI -pfglpqrsm
]
[
.BI -at
]
[
.I file
]
.SH DESCRIPTION
.I 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 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.
.PP
Given a model system specified in Promela,
.I 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.
.PP
Without any options the program performs a random simulation.
With option
.TP
.BI -n N
the seed for the simulation is set explicitly to the integer value
.BR N .
.PP
A second group of options
.B -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.
.TP
.B p
Show at each time step which process changed state.
.TP
.B l
In combination with option
.BR p ,
show the current value of local variables of the process.
.TP
.B g
Show at each time step the current value of global variables.
.TP
.B 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.
.TP
.B s
Show all message-send events.
.PP
Two options can be used to alter the model definition itself.
.TP
.B 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
.TP
.B q
Causes spin to inspect the Promela code for sequences that
can safely be cast into atomic sequences, to allow a
reduction of the complexity of larger validation runs.
Manual placement of atomic sequences can usually achieve
still larger reductions.
.B -a
(see below).
.TP
.B a
Generate a protocol-specific analyzer.
The output is written into a set of C files, named
.BR pan. [ cbhmt ],
that can be compiled
.RB ( "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:
.IP
.B cc -DBITSTATE pan.c
.IP
This collapses the state space to 1 bit per system state,
with minimal side-effects.
.IP
A compiled analyzer has its own set of options,
which can be seen by typing
.BR "a.out -?" .
.TP
.B t
If the analyzer finds a violation of an assertion, a deadlock,
a non-progress loop, or
an unspecified reception, it writes an error trail into a file
named
.BR pan.trail .
The trail can be inspected in detail by invoking
.I spin
with the
.B t
option.
In combination with the options
.B pglrs
different views of the error sequence are then easily obtained.
.SH SEE ALSO
.I cospan
in
.IR langs (1)
.br
G.J. Holzmann,
`Spin \(em A Protocol Analyzer',
this manual, Volume 2.