- verification tool for concurrent systems
spin -a [-m] [-Pcpp] file
spin -A file
spin [-bglmprsv] [-J] [-qN] [-nN] [-Pcpp] file
spin -c [-t] [-Pcpp] file
spin -d [-Pcpp] file
spin -f LTL
spin -F file
spin -i [-bglmprsv] [-J] [-qN] [-Pcpp] file
spin -M [-t] [-Pcpp] file
spin -o1 -o2 -o3 file
spin -t[N] [-bglmprsv] [-J] [-qN] [-Pcpp] file
Spin is a tool for analyzing the logical consistency of
asynchronous systems, specifically distributed software
and communication protocols.
A verification model of the system is first specified
in a guarded command language called Promela.
This specification language, described in the reference,
allows for the modeling of dynamic creation of
nondeterministic case selection, loops, gotos, local and
It also allows for a concise specification of logical
correctness requirements, including, but not restricted
to requirements expressed in linear temporal logic.
Given a Promela model stored in
Spin can perform interactive, guided, or random simulations
of the system's execution.
It can also generate a C program that performs an exhaustive
or approximate verification of the correctness requirements
for the system.
The following group of options controls which optimizations
from version 3.3 and later are enabled or disabled. By default most of
the important optimizations are enabled.
Generate a verifier (model checker) for the specification.
The output is written into a set of C files, named
pan.[ cbhmt ]
that can be compiled, (e.g.,
cc pan.c )
to produce an executable verifier.
The online Spin manuals (see below) contain
the details on compilation and use of the verifiers.
Perform property-based slicing, warning the user of all
statements and data objects that are likely to be redundant
for the stated properties (i.e., in assertions and never
claims). (Requires Spin version 3.4.0 or later.)
Produce an ASCII approximation of a message sequence
chart for a random or guided (when combined with -t)
simulation run. See also option -M.
-d Produce symbol table information for the model specified in
For each Promela object this information includes the type, name and
number of elements (if declared as an array), the initial
value (if a data object) or size (if a message channel), the
scope (global or local), and whether the object is declared as
a variable or as a parameter. For message channels, the data types
of the message fields are listed.
For structure variables, the 3rd field defines the
name of the structure declaration that contains the variable.
Translate the LTL formula LTL into a never claim.
This option reads a formula in LTL syntax from the second argument
and translates it into Promela syntax (a never claim, qhich is Promela's
equivalent of a Buchi Automaton).
The LTL operators are written:  (always), <> (eventually),
and U (strong until). There is no X (next) operator, to secure
compatibility with the partial order reduction rules that are
applied during the verification process.
If the formula contains spaces, it should be quoted to form a
single argument to the Spin command.
This behaves identical to option -f but will read the formula
from the file instead of from the command line.
The file should contain the formula as the first line. Any text
that follows this first line is ignored, so it can be used to
store comments or annotation on the formula.
(On some systems the quoting conventions of the shell complicate
the use of option -f. Option -F is meant to solve
-i Perform an interactive simulation, prompting the user at
every execution step that requires a nondeterministic choice
to be made. The simulation proceeds without user intervention
when execution is deterministic.
-J Reverse the evaluation order of nested 'unless' statements
(so that it conforms to the evaluation order of nested 'catch'
statements in Java).
-M Produce a message sequence chart in Postscript form for a
random simulation or a guided simulation
(when combined with -t), for the model in
and write the result into
See also option -c.
-m Changes the semantics of send events.
Ordinarily, a send action will be (blocked) if the
target message buffer is full.
With this option a message sent to a full buffer is lost.
Set the seed for a random simulation to the integer value
There is no space between the -n and the integer N.
-t[N] Perform a guided simulation,
following the error trail that
was produces by an earlier verification run, see the online manuals
for the details on verification.
If an optional number is attached (no space between the number and
the -t) the error trail with that sequence number is opened,
instead of the default trail, without sequence number.
-V Prints the Spin version number and exits.
disable dataflow-optimizations in verifier.
this marks variables as temporarily dead when they cannot
be read before written. their value is then reset to zero,
in an attempt to avoid redundant values in the state-vector.
in rare cases, this option can increase complexity (by adding
the zero value where it did not appear before).
disable dead variables elimination in verifier (should never
be necessary, other than to confirm its effect on the length
of the state vector and reduction of memory requirements).
disable statement merging in verifier. this option can
make it harder to read the pan -d output (of the internal
state machines used in the verifier). disabling it restores
the old, more explicit, format, but loses the advantage of
statement merging during model checking.
enable rendez-vous optimizations (experimental).
this attempts to precompute the feasibility of a rendez-vous
operation, rather than letting the model checker determine
this at run-time. we have been unable to see a positive effect
on runtime when this option is enabled, so it is likely to
disable case caching (having this option enabled
makes smarter use of the case-statements in the
pan.m and pan.b files, and allows for faster
compilation times; disable only when bugs are
With only a filename as an argument and no option flags,
Spin performs a random simulation of the model specified in
the file (standard input is the default if the filename is omitted).
This normally does not generate output, except what is generated
explicitly by the user within the model with printf
statements, and some details about the final state that is
reached after the simulation completes.
The groups of options
-bglmprsv and -qN
are used to set the desired level of information that the user wants
about a random, guided, or interactive simulation run.
Every line of output normally contains a reference to the source
line in the specification that generated it.
is added, the simulation is interactive, or if option
is added, the simulation is guided.
-b Suppresses the execution of printf statements within the model.
-B Suppresses the verbose printout at the end of a simulation
run (giving process states etc.).
-g Shows at each time step the current value of global variables.
-l In combination with option
-p, shows the current value of local variables of the process.
-p Shows at each simulation step which process changed state,
and what source statement was executed.
In columnated output (option -c) and elsewhere, suppress the
printing of output for send or receive operations on the channel
-r Shows 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.
-s Shows all message-send events.
-v Verbose mode, adds some more detail, and generates more
hints and warnings about the model.
More background information on the system and the verification process,
can be found in:
G.J. Holzmann, Design and Validation of Computer Protocols,
Prentice Hall, 1991.
--, `The model checker Spin,'
IEEE Trans. on SE, Vol, 23, No. 5, May 1997.