Subversion Repositories planix.SVN

.TH SPIN 1

.SH NAME

spin - verification tool for models of concurrent systems

.SH SYNOPSIS

.B spin

[

.I options

]

.I file

.br

.B spin

.B -V

.SH DESCRIPTION

.I 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, 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

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 --").

.

.TF -Exxx

.PD

.TP

.B -a

Generate a verifier (a 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 contain

the details on compilation and use of the verifiers.

.

.TP

.B -b

Do not execute

.I printf

statements in a simulation run.

.

.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 -Dxxx

Pass

.I -Dxxx

to the preprocessor (see also

.I -E

and

.IR -I ).

.

.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

.B -Exxx

Pass

.I xxx

to the preprocessor (see also

.I -D

and

.IR -I ).

.

.TP

.B -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.

.

.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.

.br

This option has largely been replaced with the support

for inline specification of ltl formula, in Spin version 6.0.

.

.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 -g

In combination with option

.BR -p ,

print all global variable updates in a simulation run.

.

.TP

.B -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

.B -n

option, the exact

run can be repeated later.

.

.TP

.B -I

Show the result of inlining and preprocessing.

.

.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

.BI -j N

Skip printing for the first

.I N

steps in a simulation run.

.

.TP

.B -J

Reverse the evaluation order for nested unless statements,

e.g., to match the way in which Java handles exceptions.

.

.TP

.BI -k " file"

Use the file name

.I file

as the trail-file, see also

.BR -t .

.

.TP

.B -l

In combination with option

.BR -p ,

include all local variable updates in the output of a simulation run.

.

.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

.BI -N " file"

Use the never claim stored in

.I file

to generate the verified (see

.BR -a ).

.

.TP

.BI -O

Use the original scope rules from pre-Spin version 6.

.

.TP

.BI -o [123]

Turn off data-flow optimization (

.IR -o1 ).

Do not hide write-only variables (

.I -o2

) during verification.

Turn off statement merging (

.I -o3

) during verification.

Turn on rendezvous optimization (

.I -o4

) during verification.

Turn on case caching (

.I -o5

) to reduce the size of pan.m,

but losing accuracy in reachability reports.

.

.TP

.BI -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.

.

.TP

.BI -P xxx

Use the command

.I xxx

for preprocessing instead of the standard C preprocessor.

.

.TP

.B -p

Include all statement executions in the output of simulation runs.

.

.TP

.BI -q N

Suppress the output generated for channel

.B N

during simulation runs.

.

.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

Include all send operations in the output of simulation runs.

.

.TP

.B -T

Do not automatically indent the

.I printf

output of process

.I i

with

.I i

tabs.

.

.TP

.B -t[\f2N\f1]

Perform a guided simulation, following the [\f2N\f1th] 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

.BR -k .

.

.TP

.B -v

Verbose mode, add some more detail, and generate more

hints and warnings about the model.

.

.TP

.B -V

Prints the

.I spin

version number and exit.

.

.PP

With only a filename as an argument and no option flags,

.I 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

.I printf

statements, and some details about the final state that is

reached after the simulation completes.

The group of options

.B -bgilmprstv

is 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.

If option

.B -i

is included, the simulation i

.IR interactive ,

or if option

.B -t

or

.BI -k file

is added, the simulation is

.IR guided .

.

.SH SOURCE

.B /sys/src/cmd/spin

.SH SEE ALSO

.in +4

.ti -4

.B http://spinroot.com/spin/Man/

.br

.in -4

G.J. Holzmann,

.IR "The Spin Model Checker (Primer and Reference Manual)" ,

Addison-Wesley, Reading, Mass., 2004.

.br

—, `The model checker Spin,'

.IR "IEEE Trans. on SE" ,

Vol, 23, No. 5, May 1997.

.br

—, `Design and validation of protocols: a tutorial,'

.IR "Computer Networks and ISDN Systems" ,

Vol. 25, No. 9, 1993, pp. 981-1017.

.br

—,

.IR "Design and Validation of Computer Protocols" ,

Prentice Hall, Englewood Cliffs, NJ, 1991.