Return to spin.1 CVS log

Up to [Research Unix] / researchv10dc / man / adm / man1

researchv10 Dan Cross

.TH SPIN 1
.CT 1 comm_mach protocol
.SH NAME
spin \(mi protocol analysis software
.SH SYNOPSIS
.B spin
[
.BI -n N
]
[
.BI -pglprs
]
[
.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 and deletion of both processes
and message channels, nondeterministic case selection, loops, gotos,
variables and assertions.
.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.
.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
The 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.
.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.
For larger systems the state space can quickly exhaust
the available memory on the machine used.
Large to very large systems can still be analyzed by compiling
with a bit state space:
.IP
.B cc -DBITSTATE pan.c
.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, 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.

This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.