4 .\" On CYGWIN move this page to c:/cygwin/usr/man/man1/spin.1
7 .CT 1 comm_mach protocol
9 spin \(mi verification tool for models of concurrent systems
19 .BI "[-bglmprsv] [-n\f2N\f(BI]"
48 .BI "-i [-bglmprsv] [-n\f2N\f(BI]"
62 .BI "-t[N] [-bglmprsv] [-j\f2N\f(BI]"
73 is a tool for analyzing the logical consistency of
74 asynchronous systems, specifically distributed software
75 amd communication protocols.
76 A verification model of the system is first specified
77 in a guarded command language called Promela.
78 This specification language, described in the reference,
79 allows for the modeling of dynamic creation of
80 asynchronous processes,
81 nondeterministic case selection, loops, gotos, local and
83 It also allows for a concise specification of logical
84 correctness requirements, including, but not restricted
85 to requirements expressed in linear temporal logic.
90 \*Z can perform interactive, guided, or random simulations
91 of the system's execution.
92 It can also generate a C program that performs an exhaustive
93 or approximate verification of the correctness requirements
95 .\"----------------------a----------------
98 Generate a verifier (model checker) for the specification.
99 The output is written into a set of C files, named
103 to produce an executable verifier.
104 The online \*Z manuals (see below) contain
105 the details on compilation and use of the verifiers.
106 .\"--------------------------c------------
109 Produce an ASCII approximation of a message sequence
110 chart for a random or guided
\19(when combined with \f3-t\f1)
111 simulation run. See also option \f3-M\f1.
112 .\"--------------------------d------------
115 Produce symbol table information for the model specified in
117 For each Promela object this information includes the type, name and
118 number of elements (if declared as an array), the initial
119 value (if a data object) or size (if a message channel), the
120 scope (global or local), and whether the object is declared as
121 a variable or as a parameter. For message channels, the data types
122 of the message fields are listed.
123 For structure variables, the 3rd field defines the
124 name of the structure declaration that contains the variable.
125 .\"--------------------------f------------
128 Translate the LTL formula \f2LTL\f1 into a never claim.
130 This option reads a formula in LTL syntax from the second argument
131 and translates it into Promela syntax (a never claim, qhich is Promela's
132 equivalent of a B\(u"chi Automaton).
133 The LTL operators are written: [] (always), <> (eventually),
134 and U (strong until). There is no X (next) operator, to secure
135 compatibility with the partial order reduction rules that are
136 applied during the verification process.
137 If the formula contains spaces, it should be quoted to form a
138 single argument to the \*Z command.
139 .\"--------------------------F------------
142 Translate the LTL formula stored in
146 This behaves identical to option
148 but will read the formula from the
150 instead of from the command line.
151 The file should contain the formula as the first line. Any text
152 that follows this first line is ignored, so it can be used to
153 store comments or annotation on the formula.
154 (On some systems the quoting conventions of the shell complicate
159 is meant to solve those problems.)
160 .\"--------------------------i------------
163 Perform an interactive simulation, prompting the user at
164 every execution step that requires a nondeterministic choice
165 to be made. The simulation proceeds without user intervention
166 when execution is deterministic.
167 .\"--------------------------M------------
170 Produce a message sequence chart in Postscript form for a
171 random simulation or a guided simulation
172 (when combined with \f(BI-t\f1), for the model in
174 and write the result into
176 See also option \f3-c\f1.
177 .\"--------------------------m------------
180 Changes the semantics of send events.
181 Ordinarily, a send action will be (blocked) if the
182 target message buffer is full.
183 With this option a message sent to a full buffer is lost.
184 .\"--------------------------n------------
187 Set the seed for a random simulation to the integer value
189 There is no space between the \f(BI-n\f1 and the integer \f2N\f1.
190 .\"--------------------------t------------
193 Perform a guided simulation, following the error trail that
194 was produces by an earlier verification run, see the online manuals
195 for the details on verification.
196 .\"--------------------------V------------
199 Prints the \*Z version number and exits.
200 .\"--------------------------.------------
202 With only a filename as an argument and no option flags,
203 \*Z performs a random simulation of the model specified in
204 the file (standard input is the default if the filename is omitted).
205 This normally does not generate output, except what is generated
206 explicitly by the user within the model with \f(CWprintf\f1
207 statements, and some details about the final state that is
208 reached after the simulation completes.
211 is used to set the desired level of information that the user wants
212 about a random, guided, or interactive simulation run.
213 Every line of output normally contains a reference to the source
214 line in the specification that generated it.
217 is added, the simulation is \f2interactive\f1, or if option
219 is added, the simulation is \f2guided\f1.
220 .\"--------------------------bglprsv------------
223 Suppress the execution of \f(CWprintf\f1 statements within the model.
226 Show at each time step the current value of global variables.
229 In combination with option
231 show the current value of local variables of the process.
234 Show at each simulation step which process changed state,
235 and what source statement was executed.
238 Show all message-receive events, giving
239 the name and number of the receiving process
240 and the corresponding the source line number.
241 For each message parameter, show
242 the message type and the message channel number and name.
245 Show all message-send events.
248 Verbose mode, add some more detail, and generat more
249 hints and warnings about the model.
251 Online manuals at spinroot.com:
260 More background information on the system and the verification process,
261 can be found in, for instance:
264 G.J. Holzmann, \f2Design and Validation of Computer Protocols\f1,
267 --, `Design and validation of protocols: a tutorial,'
268 \f2Computer Networks and ISDN Systems\f1,
269 Vol. 25, No. 9, 1993, pp. 981-1017.
271 --, `The model checker \*Z,'
272 \f2IEEE Trans. on SE\f1, Vol, 23, No. 5, May 1997.