1 files changed, 134 insertions, 0 deletions
diff --git a/static/unix-v10/man1/spin.1 b/static/unix-v10/man1/spin.1
new file mode 100644
index 00000000..5a6f338f
--- /dev/null
+++ b/static/unix-v10/man1/spin.1
@@ -0,0 +1,134 @@
+.TH SPIN 1
+.CT 1 comm_mach protocol
+.SH NAME
+spin \(mi protocol analysis software
+.SH SYNOPSIS
+.B spin
+[
+.BI -n N
+]
+[
+.BI -pfglpqrsm
+]
+[
+.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 of processes,
+nondeterministic case selection, loops, gotos,
+variables and assertions.
+The tool has fast and frugal algorithms for analyzing
+liveness and safeness conditions.
+.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, or
+if any non-progress execution cycles exist.
+.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
+A 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.
+.PP
+Two options can be used to alter the model definition itself.
+.TP
+.B m
+Changes the semantics of send events.
+Ordinarily, a send action will be delayed if the
+target message buffer if full.
+With this option a message sent to a full buffer is lost.
+The option can be combined with
+.TP
+.B q
+Causes spin to inspect the Promela code for sequences that
+can safely be cast into atomic sequences, to allow a
+reduction of the complexity of larger validation runs.
+Manual placement of atomic sequences can usually achieve
+still larger reductions.
+.B -a
+(see below).
+.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.
+Large systems, that require more memory than available
+on the target machine, can still be analyzed by compiling
+the analyzer with a bit state space:
+.IP
+.B cc -DBITSTATE pan.c
+.IP
+This collapses the state space to 1 bit per system state,
+with minimal side-effects.
+.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,
+a non-progress loop, 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.