sys/man/1/spin

   1 .TH SPIN 1
   2 .SH NAME
   3 spin - verification tool for models of concurrent systems
   4 .SH SYNOPSIS
   5 .B spin
   6 .B -a
   7 [
   8 .B -m
   9 ]
  10 [
  11 .BI -P cpp
  12 ]
  13 .I file
  14 .PP
  15 .B spin
  16 [
  17 .B -bglmprsv
  18 ]
  19 [
  20 .BI -n N
  21 ]
  22 [
  23 .BI -P cpp
  24 ]
  25 .I file
  26 .PP
  27 .B spin
  28 .B -c
  29 [
  30 .B -t
  31 ]
  32 [
  33 .BI -P cpp
  34 ]
  35 .I file
  36 .PP
  37 .B spin
  38 .B -d
  39 [
  40 .BI -P cpp
  41 ]
  42 .I file
  43 .PP
  44 .B spin
  45 .B -f
  46 .I ltl
  47 .PP
  48 .B spin
  49 .B -F
  50 .I file
  51 .PP
  52 .B spin
  53 .B -i
  54 [
  55 .B -bglmprsv
  56 ]
  57 [
  58 .BI -n N
  59 ]
  60 [
  61 .BI -P cpp
  62 ]
  63 .I file
  64 .PP
  65 .B spin
  66 .B -M
  67 [
  68 .B -t
  69 ]
  70 [
  71 .BI -P cpp
  72 ]
  73 .I file
  74 .PP
  75 .B spin
  76 .BR -t [ \fIN ]
  77 [
  78 .B -bglmprsv
  79 ]
  80 [
  81 .BI -j N
  82 ]
  83 [
  84 .BI -P cpp
  85 ]
  86 .I file
  87 .PP
  88 .B spin
  89 .B -V
  90 .SH DESCRIPTION
  91 .I Spin
  92 is a tool for analyzing the logical consistency of
  93 asynchronous systems, specifically distributed software
  94 and communication protocols.
  95 A verification model of the system is first specified
  96 in a guarded command language called
  97 .IR Promela .
  98 This specification language, described in the reference,
  99 allows for the modeling of dynamic creation of
 100 asynchronous processes,
 101 nondeterministic case selection, loops, gotos, local and
 102 global variables.
 103 It also allows for a concise specification of logical
 104 correctness requirements, including, but not restricted
 105 to, requirements expressed in linear temporal logic.
 106 .PP
 107 Given a Promela model stored in
 108 .IR file ,
 109 .I spin
 110 can perform interactive, guided, or random simulations
 111 of the system's execution.
 112 It can also generate a C program that performs an exhaustive
 113 or approximate verification of the correctness requirements
 114 for the system.
 115 .
 116 .TP
 117 .B -a
 118 Generate a verifier (model checker) for the specification.
 119 The output is written into a set of C files, named
 120 .BR pan.[cbhmt] ,
 121 that can be compiled
 122 .RB ( "pcc pan.c" )
 123 to produce an executable verifier.
 124 The online
 125 .I spin
 126 manuals (see below) contain
 127 the details on compilation and use of the verifiers.
 128 .
 129 .TP
 130 .B -c
 131 Produce an ASCII approximation of a message sequence
 132 chart for a random or guided (when combined with
 133 .BR -t )
 134 simulation run. See also option
 135 .BR -M .
 136 .
 137 .TP
 138 .B -d
 139 Produce symbol table information for the model specified in
 140 .IR file .
 141 For each Promela object this information includes the type, name and
 142 number of elements (if declared as an array), the initial
 143 value (if a data object) or size (if a message channel), the
 144 scope (global or local), and whether the object is declared as
 145 a variable or as a parameter.  For message channels, the data types
 146 of the message fields are listed.
 147 For structure variables, the third field defines the
 148 name of the structure declaration that contains the variable.
 149 .
 150 .TP
 151 .BI -f " ltl"
 152 Translate the LTL formula
 153 .I ltl
 154 into a
 155 .I never
 156 claim.
 157 .br
 158 This option reads a formula in LTL syntax from the second argument
 159 and translates it into Promela syntax (a
 160 .I never
 161 claim, which is Promela's
 162 equivalent of a Büchi Automaton).
 163 The LTL operators are written:
 164 .B []
 165 (always),
 166 .B <>
 167 (eventually),
 168 and
 169 .B U
 170 (strong until).  There is no
 171 .B X
 172 (next) operator, to secure
 173 compatibility with the partial order reduction rules that are
 174 applied during the verification process.
 175 If the formula contains spaces, it should be quoted to form a
 176 single argument to the
 177 .I spin
 178 command.
 179 .
 180 .TP
 181 .BI -F " file"
 182 Translate the LTL formula stored in
 183 .I file
 184 into a
 185 .I never
 186 claim.
 187 .br
 188 This behaves identically to option
 189 .B -f
 190 but will read the formula from the
 191 .I file
 192 instead of from the command line.
 193 The file should contain the formula as the first line.  Any text
 194 that follows this first line is ignored, so it can be used to
 195 store comments or annotation on the formula.
 196 (On some systems the quoting conventions of the shell complicate
 197 the use of option
 198 .BR -f .
 199 Option
 200 .B -F
 201 is meant to solve those problems.)
 202 .
 203 .TP
 204 .B -i
 205 Perform an interactive simulation, prompting the user at
 206 every execution step that requires a nondeterministic choice
 207 to be made.  The simulation proceeds without user intervention
 208 when execution is deterministic.
 209 .
 210 .TP
 211 .B -M
 212 Produce a message sequence chart in Postscript form for a
 213 random simulation or a guided simulation
 214 (when combined with
 215 .BR -t ),
 216 for the model in
 217 .IR file ,
 218 and write the result into
 219 .IR file.ps .
 220 See also option
 221 .BR -c .
 222 .
 223 .TP
 224 .B -m
 225 Changes the semantics of send events.
 226 Ordinarily, a send action will be (blocked) if the
 227 target message buffer is full.
 228 With this option a message sent to a full buffer is lost.
 229 .
 230 .TP
 231 .BI -n N
 232 Set the seed for a random simulation to the integer value
 233 .IR N .
 234 There is no space between the
 235 .B -n
 236 and the integer
 237 .IR N .
 238 .
 239 .TP
 240 .B -t
 241 Perform a guided simulation, following the error trail that
 242 was produces by an earlier verification run, see the online manuals
 243 for the details on verification.
 244 .
 245 .TP
 246 .B -V
 247 Prints the
 248 .I spin
 249 version number and exits.
 250 .
 251 .PP
 252 With only a filename as an argument and no options,
 253 .I spin
 254 performs a random simulation of the model specified in
 255 the file (standard input is the default if the filename is omitted).
 256 If option
 257 .B -i
 258 is added, the simulation is
 259 .IR interactive ,
 260 or if option
 261 .B -t
 262 is added, the simulation is
 263 .IR guided .
 264 .PP
 265 The simulation normally does not generate output, except what is generated
 266 explicitly by the user within the model with
 267 .I printf
 268 statements, and some details about the final state that is
 269 reached after the simulation completes.
 270 The group of options
 271 .B -bglmprsv
 272 sets the desired level of information that the user wants
 273 about a random, guided, or interactive simulation run.
 274 Every line of output normally contains a reference to the source
 275 line in the specification that generated it.
 276 .
 277 .TP
 278 .B -b
 279 Suppress the execution of
 280 .I printf
 281 statements within the model.
 282 .TP
 283 .B -g
 284 Show at each time step the current value of global variables.
 285 .TP
 286 .B -l
 287 In combination with option
 288 .BR -p ,
 289 show the current value of local variables of the process.
 290 .TP
 291 .B -p
 292 Show at each simulation step which process changed state,
 293 and what source statement was executed.
 294 .TP
 295 .B -r
 296 Show all message-receive events, giving
 297 the name and number of the receiving process
 298 and the corresponding the source line number.
 299 For each message parameter, show
 300 the message type and the message channel number and name.
 301 .TP
 302 .B -s
 303 Show all message-send events.
 304 .TP
 305 .B -v
 306 Verbose mode, add some more detail, and generate more
 307 hints and warnings about the model.
 308 .SH SOURCE
 309 .B /sys/src/cmd/spin
 310 .SH SEE ALSO
 311 .in +4
 312 .ti -4
 313 .BR http://spinroot.com :
 314 .BR GettingStarted.pdf ,
 315 .BR Roadmap.pdf ,
 316 .BR Manual.pdf ,
 317 .BR WhatsNew.pdf ,
 318 .B Exercises.pdf
 319 .br
 320 .in -4
 321 G.J. Holzmann,
 322 .IR "Design and Validation of Computer Protocols" ,
 323 Prentice Hall, 1991.
 324 .br
 325 —, `Design and validation of protocols: a tutorial,'
 326 .IR "Computer Networks and ISDN Systems" ,
 327 Vol. 25, No. 9, 1993, pp. 981-1017.
 328 .br
 329 —, `The model checker Spin,'
 330 .IR "IEEE Trans. on SE" ,
 331 Vol, 23, No. 5, May 1997.