SPIN(1)SPIN(1)NAMEspin - verification tool for models of concurrent systems
SYNOPSISspin [ options ] file
spin-V
DESCRIPTION
Spin is a tool for analyzing the logical consistency of asynchronous
systems, specifically distributed software, multi-threaded systems, and
communication protocols. A model of the system is specified in a
guarded command language called Promela (process meta language). This
modeling language supports dynamic creation of processes, nondetermin‐
istic case selection, loops, gotos, local and global variables. It
also allows for a concise specification of logical correctness require‐
ments, including, but not restricted to requirements expressed in lin‐
ear temporal logic.
Given a Promela model stored in file, spin can perform interactive,
guided, or random simulations of the system's execution. It can also
generate a C program that performs an exhaustive verification of the
correctness requirements for the system. The main options supported
are as follows. (You can always get a full list of current options with
the command "spin --").
-a Generate a verifier (a model checker) for the specification.
The output is written into a set of C files named pan.[cbhmt],
that can be compiled (pcc pan.c) to produce an executable veri‐
fier. The online spin manuals contain the details on compila‐
tion and use of the verifiers.
-b Do not execute printf statements in a simulation run.
-c Produce an ASCII approximation of a message sequence chart for a
random or guided (when combined with -t) simulation run. See
also option -M.
-Dxxx Pass -Dxxx to the preprocessor (see also -E and -I).
-d Produce symbol table information for the model specified in
file. 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 vari‐
ables, the third field defines the name of the structure decla‐
ration that contains the variable.
-Exxx Pass xxx to the preprocessor (see also -D and -I).
-e If the specification contains multiple never claims, or ltl
properties, compute the synchronous product of all claims and
write the result to the standard output.
-f ltl Translate the LTL formula ltl into a never claim.
This option reads a formula in LTL syntax from the second argu‐
ment and translates it into Promela syntax (a never claim, which
is Promela's equivalent of a Büchi Automaton). The LTL opera‐
tors 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 option has largely been replaced with the support for
inline specification of ltl formula, in Spin version 6.0.
-F file
Translate the LTL formula stored in file into a never claim.
This behaves identically 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 con‐
ventions of the shell complicate the use of option -f. Option
-F is meant to solve those problems.)
-g In combination with option -p, print all global variable updates
in a simulation run.
-h At the end of a simulation run, print the value of the seed that
was used for the random number generator. By specifying the
same seed with the -n option, the exact run can be repeated
later.
-I Show the result of inlining and preprocessing.
-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.
-jN Skip printing for the first N steps in a simulation run.
-J Reverse the evaluation order for nested unless statements, e.g.,
to match the way in which Java handles exceptions.
-k file
Use the file name file as the trail-file, see also -t.
-l In combination with option -p, include all local variable
updates in the output of a simulation run.
-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 file, and write the result into file.ps. 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.
-nN Set the seed for a random simulation to the integer value N.
There is no space between the -n and the integer N.
-N file
Use the never claim stored in file to generate the verified (see
-a).
-O Use the original scope rules from pre-Spin version 6.
-o[123]
Turn off data-flow optimization ( -o1). Do not hide write-only
variables ( -o2 ) during verification. Turn off statement merg‐
ing ( -o3 ) during verification. Turn on rendezvous optimiza‐
tion ( -o4 ) during verification. Turn on case caching ( -o5 )
to reduce the size of pan.m, but losing accuracy in reachability
reports.
-O Use the scope rules pre-version 6.0. In this case there are only
two possible levels of scope for all data declarations: global,
or proctype local. In version 6.0 and later there is a third
level of scope: inlines or blocks.
-Pxxx Use the command xxx for preprocessing instead of the standard C
preprocessor.
-p Include all statement executions in the output of simulation
runs.
-qN Suppress the output generated for channel N during simulation
runs.
-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 Include all send operations in the output of simulation runs.
-T Do not automatically indent the printf output of process i with
i tabs.
-t[N] Perform a guided simulation, following the [Nth] error trail
that was produces by an earlier verification run, see the online
manuals for the details on verification. By default the error
trail is looked for in a file with the same basename as the
model, and with extension .trail. See also -k.
-v Verbose mode, add some more detail, and generate more hints and
warnings about the model.
-V Prints the spin version number and exit.
With only a filename as an argument and no option flags, spin performs
a random simulation of the model specified in the file. 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
group of options -bgilmprstv is used to set the desired level of infor‐
mation that the user wants about a random, guided, or interactive simu‐
lation run. Every line of output normally contains a reference to the
source line in the specification that generated it. If option -i is
included, the simulation i interactive, or if option -t or -kfile is
added, the simulation is guided.
SOURCE
/sys/src/cmd/spin
SEE ALSO
http://spinroot.com/spin/Man/
G.J. Holzmann, The Spin Model Checker (Primer and Reference Manual),
Addison-Wesley, Reading, Mass., 2004.
—, `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No. 5, May
1997.
—, `Design and validation of protocols: a tutorial,' Computer Networks
and ISDN Systems, Vol. 25, No. 9, 1993, pp. 981-1017.
—, Design and Validation of Computer Protocols, Prentice Hall, Engle‐
wood Cliffs, NJ, 1991.
SPIN(1)
