.TH SPIN 1.SH NAMEspin - verification tool for models of concurrent systems.SH SYNOPSIS.B spin.B -a[.B -m][.BI -P cpp].I file.PP.B spin[.B -bglmprsv][.BI -n N][.BI -P cpp].I file.PP.B spin.B -c[.B -t][.BI -P cpp].I file.PP.B spin.B -d[.BI -P cpp].I file.PP.B spin.B -f.I ltl.PP.B spin.B -F.I file.PP.B spin.B -i[.B -bglmprsv][.BI -n N][.BI -P cpp].I file.PP.B spin.B -M[.B -t][.BI -P cpp].I file.PP.B spin.BR -t [ \fIN ][.B -bglmprsv][.BI -j N][.BI -P cpp].I file.PP.B spin.B -V.SH DESCRIPTION.I Spinis a tool for analyzing the logical consistency ofasynchronous systems, specifically distributed softwareamd communication protocols.A verification model of the system is first specifiedin a guarded command language called.IR Promela .This specification language, described in the reference,allows for the modeling of dynamic creation ofasynchronous processes,nondeterministic case selection, loops, gotos, local andglobal variables.It also allows for a concise specification of logicalcorrectness requirements, including, but not restrictedto requirements expressed in linear temporal logic..PPGiven a Promela model stored in.IR file ,.I spincan perform interactive, guided, or random simulationsof the system's execution.It can also generate a C program that performs an exhaustiveor approximate verification of the correctness requirementsfor the system...TP.B -aGenerate a verifier (model checker) for the specification.The output is written into a set of C files, named.BR pan.[cbhmt] ,that can be compiled.RB ( "pcc pan.c" )to produce an executable verifier.The online.I spinmanuals (see below) containthe details on compilation and use of the verifiers...TP.B -cProduce an ASCII approximation of a message sequencechart for a random or guided (when combined with.BR -t )simulation run. See also option.BR -M ...TP.B -dProduce symbol table information for the model specified in.IR file .For each Promela object this information includes the type, name andnumber of elements (if declared as an array), the initialvalue (if a data object) or size (if a message channel), thescope (global or local), and whether the object is declared asa variable or as a parameter. For message channels, the data typesof the message fields are listed.For structure variables, the third field defines thename of the structure declaration that contains the variable...TP.BI -f " ltl"Translate the LTL formula.I ltlinto a.I neverclaim..brThis option reads a formula in LTL syntax from the second argumentand translates it into Promela syntax (a.I neverclaim, which is Promela'sequivalent of a Büchi Automaton).The LTL operators are written:.B [](always),.B <>(eventually),and.B U(strong until). There is no.B X(next) operator, to securecompatibility with the partial order reduction rules that areapplied during the verification process.If the formula contains spaces, it should be quoted to form asingle argument to the.I spincommand...TP.BI -F " file"Translate the LTL formula stored in.I fileinto a.I neverclaim..brThis behaves identically to option.B -fbut will read the formula from the.I fileinstead of from the command line.The file should contain the formula as the first line. Any textthat follows this first line is ignored, so it can be used tostore comments or annotation on the formula.(On some systems the quoting conventions of the shell complicatethe use of option.BR -f .Option.B -Fis meant to solve those problems.)..TP.B -iPerform an interactive simulation, prompting the user atevery execution step that requires a nondeterministic choiceto be made. The simulation proceeds without user interventionwhen execution is deterministic...TP.B -MProduce a message sequence chart in Postscript form for arandom simulation or a guided simulation(when combined with.BR -t ),for the model in.IR file ,and write the result into.IR file.ps .See also option.BR -c ...TP.B -mChanges the semantics of send events.Ordinarily, a send action will be (blocked) if thetarget message buffer is full.With this option a message sent to a full buffer is lost...TP.BI -n NSet the seed for a random simulation to the integer value.IR N .There is no space between the.B -nand the integer.IR N ...TP.B -tPerform a guided simulation, following the error trail thatwas produces by an earlier verification run, see the online manualsfor the details on verification...TP.B -VPrints the.I spinversion number and exits...PPWith only a filename as an argument and no options,.I spinperforms a random simulation of the model specified inthe file (standard input is the default if the filename is omitted).If option.B -iis added, the simulation is.IR interactive ,or if option.B -tis added, the simulation is.IR guided ..PPThe simulation normally does not generate output, except what is generatedexplicitly by the user within the model with.I printfstatements, and some details about the final state that isreached after the simulation completes.The group of options.B -bglmprsvsets the desired level of information that the user wantsabout a random, guided, or interactive simulation run.Every line of output normally contains a reference to the sourceline in the specification that generated it...TP.B -bSuppress the execution of.I printfstatements within the model..TP.B -gShow at each time step the current value of global variables..TP.B -lIn combination with option.BR -p ,show the current value of local variables of the process..TP.B -pShow at each simulation step which process changed state,and what source statement was executed..TP.B -rShow all message-receive events, givingthe name and number of the receiving processand the corresponding the source line number.For each message parameter, showthe message type and the message channel number and name..TP.B -sShow all message-send events..TP.B -vVerbose mode, add some more detail, and generate morehints and warnings about the model..SH SOURCE.B /sys/src/cmd/spin.SH SEE ALSO.in +4.ti -4.BR http://spinroot.com :.BR GettingStarted.pdf ,.BR Roadmap.pdf ,.BR Manual.pdf ,.BR WhatsNew.pdf ,.B Exercises.pdf.br.in -4G.J. Holzmann,.IR "Design and Validation of Computer Protocols" ,Prentice Hall, 1991..br—, `Design and validation of protocols: a tutorial,'.IR "Computer Networks and ISDN Systems" ,Vol. 25, No. 9, 1993, pp. 981-1017..br—, `The model checker Spin,'.IR "IEEE Trans. on SE" ,Vol, 23, No. 5, May 1997.
.TH SPIN 1
.SH NAME
spin - verification tool for models of concurrent systems
.SH SYNOPSIS
.B spin
.B -a
[
.B -m
]
[
.BI -P cpp
]
.I file
.PP
.B spin
[
.B -bglmprsv
]
[
.BI -n N
]
[
.BI -P cpp
]
.I file
.PP
.B spin
.B -c
[
.B -t
]
[
.BI -P cpp
]
.I file
.PP
.B spin
.B -d
[
.BI -P cpp
]
.I file
.PP
.B spin
.B -f
.I ltl
.PP
.B spin
.B -F
.I file
.PP
.B spin
.B -i
[
.B -bglmprsv
]
[
.BI -n N
]
[
.BI -P cpp
]
.I file
.PP
.B spin
.B -M
[
.B -t
]
[
.BI -P cpp
]
.I file
.PP
.B spin
.BR -t [ \fIN ]
[
.B -bglmprsv
]
[
.BI -j N
]
[
.BI -P cpp
]
.I file
.PP
.B spin
.B -V
.SH DESCRIPTION
.I Spin
is a tool for analyzing the logical consistency of
asynchronous systems, specifically distributed software
amd communication protocols.
A verification model of the system is first specified
in a guarded command language called
.IR Promela .
This specification language, described in the reference,
allows for the modeling of dynamic creation of
asynchronous processes,
nondeterministic case selection, loops, gotos, local and
global variables.
It also allows for a concise specification of logical
correctness requirements, including, but not restricted
to requirements expressed in linear temporal logic.
.PP
Given a Promela model stored in
.IR file ,
.I 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.
.
.TP
.B -a
Generate a verifier (model checker) for the specification.
The output is written into a set of C files, named
.BR pan.[cbhmt] ,
that can be compiled
.RB ( "pcc pan.c" )
to produce an executable verifier.
The online
.I spin
manuals (see below) contain
the details on compilation and use of the verifiers.
.
.TP
.B -c
Produce an ASCII approximation of a message sequence
chart for a random or guided (when combined with
.BR -t )
simulation run. See also option
.BR -M .
.
.TP
.B -d
Produce symbol table information for the model specified in
.IR 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 variables, the third field defines the
name of the structure declaration that contains the variable.
.
.TP
.BI -f " ltl"
Translate the LTL formula
.I ltl
into a
.I never
claim.
.br
This option reads a formula in LTL syntax from the second argument
and translates it into Promela syntax (a
.I never
claim, which is Promela's
equivalent of a Büchi Automaton).
The LTL operators are written:
.B []
(always),
.B <>
(eventually),
and
.B U
(strong until). There is no
.B 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
.I spin
command.
.
.TP
.BI -F " file"
Translate the LTL formula stored in
.I file
into a
.I never
claim.
.br
This behaves identically to option
.B -f
but will read the formula from the
.I 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
.BR -f .
Option
.B -F
is meant to solve those problems.)
.
.TP
.B -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.
.
.TP
.B -M
Produce a message sequence chart in Postscript form for a
random simulation or a guided simulation
(when combined with
.BR -t ),
for the model in
.IR file ,
and write the result into
.IR file.ps .
See also option
.BR -c .
.
.TP
.B -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.
.
.TP
.BI -n N
Set the seed for a random simulation to the integer value
.IR N .
There is no space between the
.B -n
and the integer
.IR N .
.
.TP
.B -t
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.
.
.TP
.B -V
Prints the
.I spin
version number and exits.
.
.PP
With only a filename as an argument and no options,
.I spin
performs a random simulation of the model specified in
the file (standard input is the default if the filename is omitted).
If option
.B -i
is added, the simulation is
.IR interactive ,
or if option
.B -t
is added, the simulation is
.IR guided .
.PP
The simulation normally does not generate output, except what is generated
explicitly by the user within the model with
.I printf
statements, and some details about the final state that is
reached after the simulation completes.
The group of options
.B -bglmprsv
sets 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.
.
.TP
.B -b
Suppress the execution of
.I printf
statements within the model.
.TP
.B -g
Show at each time step the current value of global variables.
.TP
.B -l
In combination with option
.BR -p ,
show the current value of local variables of the process.
.TP
.B -p
Show at each simulation step which process changed state,
and what source statement was executed.
.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.
.TP
.B -v
Verbose mode, add some more detail, and generate more
hints and warnings about the model.
.SH SOURCE
.B /sys/src/cmd/spin
.SH SEE ALSO
.in +4
.ti -4
.BR http://spinroot.com :
.BR GettingStarted.pdf ,
.BR Roadmap.pdf ,
.BR Manual.pdf ,
.BR WhatsNew.pdf ,
.B Exercises.pdf
.br
.in -4
G.J. Holzmann,
.IR "Design and Validation of Computer Protocols" ,
Prentice Hall, 1991.
.br
—, `Design and validation of protocols: a tutorial,'
.IR "Computer Networks and ISDN Systems" ,
Vol. 25, No. 9, 1993, pp. 981-1017.
.br
—, `The model checker Spin,'
.IR "IEEE Trans. on SE" ,
Vol, 23, No. 5, May 1997.