![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to spin.1 CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / man / man1|
Return to spin.1 CVS log | Up to [Research Unix] / researchv10dc / man / man1 |
1.1 root 1: .TH SPIN 1
2: .CT 1 comm_mach protocol
3: .SH NAME
4: spin \(mi protocol analysis software
5: .SH SYNOPSIS
6: .B spin
7: [
8: .BI -n N
9: ]
10: [
11: .BI -pglprsm
12: ]
13: [
14: .BI -at
15: ]
16: [
17: .I file
18: ]
19: .SH DESCRIPTION
20: .I Spin
21: is a tool for analyzing the logical consistency of
22: concurrent systems, specifically communication protocols.
23: The system is specified in a guarded command language called Promela.
24: The language, described in the reference,
25: allows for the dynamic creation of processes,
26: nondeterministic case selection, loops, gotos,
27: variables and assertions.
28: The tool has fast and frugal algorithms for analyzing
29: liveness and safeness conditions.
30: .PP
31: Given a model system specified in Promela,
32: .I spin
33: can either perform random simulations of the system's execution
34: or it can generate a C program that performs a fast exhaustive
35: validation of the system state space.
36: The validator can check, for instance, if user specified system
37: invariants may be violated during a protocol's execution, or
38: if any non-progress execution cycles exist.
39: .PP
40: Without any options the program performs a random simulation.
41: With option
42: .TP
43: .BI -n N
44: the seed for the simulation is set explicitly to the integer value
45: .BR N .
46: .PP
47: The second group of options
48: .B -pglrs
49: is used to set the desired level of information that the user wants
50: about the simulation run.
51: Every line of output normally contains a reference to the source
52: line in the specification that caused it.
53: .TP
54: .B p
55: Show at each time step which process changed state.
56: .TP
57: .B l
58: In combination with option
59: .BR p ,
60: show the current value of local variables of the process.
61: .TP
62: .B g
63: Show at each time step the current value of global variables.
64: .TP
65: .B r
66: Show all message-receive events, giving
67: the name and number of the receiving process
68: and the corresponding the source line number.
69: For each message parameter, show
70: the message type and the message channel number and name.
71: .TP
72: .B s
73: Show all message-send events.
74: .TP
75: .B m
76: Changes the semantics of send events.
77: Ordinarily, a send action will be delayed if the
78: target message buffer if full.
79: With this option a message sent to a full buffer is lost.
80: The option can be combined with
81: .B -a
82: (see below).
83: .TP
84: .B a
85: Generate a protocol-specific analyzer.
86: The output is written into a set of C files, named
87: .BR pan. [ cbhmt ],
88: that can be compiled
89: .RB ( "cc pan.c" )
90: to produce an executable analyzer.
91: Large systems, that require more memory than available
92: on the target machine, can still be analyzed by compiling
93: the analyzer with a bit state space:
94: .IP
95: .B cc -DBITSTATE pan.c
96: .IP
97: This collapses the state space to 1 bit per system state,
98: with minimal side-effects.
99: .IP
100: A compiled analyzer has its own set of options,
101: which can be seen by typing
102: .BR "a.out -?" .
103: .TP
104: .B t
105: If the analyzer finds a violation of an assertion, a deadlock,
106: a non-progress loop, or
107: an unspecified reception, it writes an error trail into a file
108: named
109: .BR pan.trail .
110: The trail can be inspected in detail by invoking
111: .I spin
112: with the
113: .B t
114: option.
115: In combination with the options
116: .B pglrs
117: different views of the error sequence are then easily obtained.
118: .SH SEE ALSO
119: .I cospan
120: in
121: .IR langs (1)
122: .br
123: G.J. Holzmann,
124: `Spin \(em A Protocol Analyzer',
125: this manual, Volume 2.
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.