spin 8.4 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380
  1. .TH SPIN 1
  2. .SH NAME
  3. spin - verification tool for models of concurrent systems
  4. .SH SYNOPSIS
  5. .B spin
  6. [
  7. .I options
  8. ]
  9. .I file
  10. .br
  11. .B spin
  12. .B -V
  13. .SH DESCRIPTION
  14. .I Spin
  15. is a tool for analyzing the logical consistency of
  16. asynchronous systems, specifically distributed software,
  17. multi-threaded systems, and communication protocols.
  18. A model of the system is specified
  19. in a guarded command language called Promela (process meta language).
  20. This modeling language supports dynamic creation of
  21. processes, nondeterministic case selection, loops, gotos,
  22. local and global variables.
  23. It also allows for a concise specification of logical
  24. correctness requirements, including, but not restricted
  25. to requirements expressed in linear temporal logic.
  26. .PP
  27. Given a Promela model stored in
  28. .IR file ,
  29. .I spin
  30. can perform interactive, guided, or random simulations
  31. of the system's execution.
  32. It can also generate a C program that performs an exhaustive
  33. verification of the correctness requirements for the system.
  34. The main options supported are as follows. (You can always get
  35. a full list of current options with the command "spin --").
  36. .
  37. .TF -Exxx
  38. .PD
  39. .TP
  40. .B -a
  41. Generate a verifier (a model checker) for the specification.
  42. The output is written into a set of C files named
  43. .BR pan.[cbhmt] ,
  44. that can be compiled
  45. .RB ( "pcc pan.c" )
  46. to produce an executable verifier.
  47. The online
  48. .I spin
  49. manuals contain
  50. the details on compilation and use of the verifiers.
  51. .
  52. .TP
  53. .B -b
  54. Do not execute
  55. .I printf
  56. statements in a simulation run.
  57. .
  58. .TP
  59. .B -c
  60. Produce an ASCII approximation of a message sequence
  61. chart for a random or guided (when combined with
  62. .BR -t )
  63. simulation run. See also option
  64. .BR -M .
  65. .
  66. .TP
  67. .B -Dxxx
  68. Pass
  69. .I -Dxxx
  70. to the preprocessor (see also
  71. .I -E
  72. and
  73. .IR -I ).
  74. .
  75. .TP
  76. .B -d
  77. Produce symbol table information for the model specified in
  78. .IR file .
  79. For each Promela object this information includes the type, name and
  80. number of elements (if declared as an array), the initial
  81. value (if a data object) or size (if a message channel), the
  82. scope (global or local), and whether the object is declared as
  83. a variable or as a parameter. For message channels, the data types
  84. of the message fields are listed.
  85. For structure variables, the third field defines the
  86. name of the structure declaration that contains the variable.
  87. .
  88. .TP
  89. .B -Exxx
  90. Pass
  91. .I xxx
  92. to the preprocessor (see also
  93. .I -D
  94. and
  95. .IR -I ).
  96. .
  97. .TP
  98. .B -e
  99. If the specification contains multiple never claims, or ltl properties,
  100. compute the synchronous product of all claims and write the result
  101. to the standard output.
  102. .
  103. .TP
  104. .BI -f " ltl"
  105. Translate the LTL formula
  106. .I ltl
  107. into a
  108. .I never
  109. claim.
  110. .br
  111. This option reads a formula in LTL syntax from the second argument
  112. and translates it into Promela syntax (a
  113. .I never
  114. claim, which is Promela's
  115. equivalent of a Büchi Automaton).
  116. The LTL operators are written:
  117. .B []
  118. (always),
  119. .B <>
  120. (eventually),
  121. and
  122. .B U
  123. (strong until). There is no
  124. .B X
  125. (next) operator, to secure
  126. compatibility with the partial order reduction rules that are
  127. applied during the verification process.
  128. If the formula contains spaces, it should be quoted to form a
  129. single argument to the
  130. .I spin
  131. command.
  132. .br
  133. This option has largely been replaced with the support
  134. for inline specification of ltl formula, in Spin version 6.0.
  135. .
  136. .TP
  137. .BI -F " file"
  138. Translate the LTL formula stored in
  139. .I file
  140. into a
  141. .I never
  142. claim.
  143. .br
  144. This behaves identically to option
  145. .B -f
  146. but will read the formula from the
  147. .I file
  148. instead of from the command line.
  149. The file should contain the formula as the first line. Any text
  150. that follows this first line is ignored, so it can be used to
  151. store comments or annotation on the formula.
  152. (On some systems the quoting conventions of the shell complicate
  153. the use of option
  154. .BR -f .
  155. Option
  156. .B -F
  157. is meant to solve those problems.)
  158. .
  159. .TP
  160. .B -g
  161. In combination with option
  162. .BR -p ,
  163. print all global variable updates in a simulation run.
  164. .
  165. .TP
  166. .B -h
  167. At the end of a simulation run, print the value of the seed
  168. that was used for the random number generator.
  169. By specifying the same seed with the
  170. .B -n
  171. option, the exact
  172. run can be repeated later.
  173. .
  174. .TP
  175. .B -I
  176. Show the result of inlining and preprocessing.
  177. .
  178. .TP
  179. .B -i
  180. Perform an interactive simulation, prompting the user at
  181. every execution step that requires a nondeterministic choice
  182. to be made. The simulation proceeds without user intervention
  183. when execution is deterministic.
  184. .
  185. .TP
  186. .BI -j N
  187. Skip printing for the first
  188. .I N
  189. steps in a simulation run.
  190. .
  191. .TP
  192. .B -J
  193. Reverse the evaluation order for nested unless statements,
  194. e.g., to match the way in which Java handles exceptions.
  195. .
  196. .TP
  197. .BI -k " file"
  198. Use the file name
  199. .I file
  200. as the trail-file, see also
  201. .BR -t .
  202. .
  203. .TP
  204. .B -l
  205. In combination with option
  206. .BR -p ,
  207. include all local variable updates in the output of a simulation run.
  208. .
  209. .TP
  210. .B -M
  211. Produce a message sequence chart in Postscript form for a
  212. random simulation or a guided simulation
  213. (when combined with
  214. .BR -t ),
  215. for the model in
  216. .IR file ,
  217. and write the result into
  218. .IR file.ps .
  219. See also option
  220. .BR -c .
  221. .
  222. .TP
  223. .B -m
  224. Changes the semantics of send events.
  225. Ordinarily, a send action will be (blocked) if the
  226. target message buffer is full.
  227. With this option a message sent to a full buffer is lost.
  228. .
  229. .TP
  230. .BI -n N
  231. Set the seed for a random simulation to the integer value
  232. .IR N .
  233. There is no space between the
  234. .B -n
  235. and the integer
  236. .IR N .
  237. .
  238. .TP
  239. .BI -N " file"
  240. Use the never claim stored in
  241. .I file
  242. to generate the verified (see
  243. .BR -a ).
  244. .
  245. .TP
  246. .BI -O
  247. Use the original scope rules from pre-Spin version 6.
  248. .
  249. .TP
  250. .BI -o [123]
  251. Turn off data-flow optimization (
  252. .IR -o1 ).
  253. Do not hide write-only variables (
  254. .I -o2
  255. ) during verification.
  256. Turn off statement merging (
  257. .I -o3
  258. ) during verification.
  259. Turn on rendezvous optimization (
  260. .I -o4
  261. ) during verification.
  262. Turn on case caching (
  263. .I -o5
  264. ) to reduce the size of pan.m,
  265. but losing accuracy in reachability reports.
  266. .
  267. .TP
  268. .BI -O
  269. Use the scope rules pre-version 6.0. In this case there are only two
  270. possible levels of scope for all data declarations: global, or proctype local.
  271. In version 6.0 and later there is a third level of scope: inlines or blocks.
  272. .
  273. .TP
  274. .BI -P xxx
  275. Use the command
  276. .I xxx
  277. for preprocessing instead of the standard C preprocessor.
  278. .
  279. .TP
  280. .B -p
  281. Include all statement executions in the output of simulation runs.
  282. .
  283. .TP
  284. .BI -q N
  285. Suppress the output generated for channel
  286. .B N
  287. during simulation runs.
  288. .
  289. .TP
  290. .B -r
  291. Show all message-receive events, giving
  292. the name and number of the receiving process
  293. and the corresponding the source line number.
  294. For each message parameter, show
  295. the message type and the message channel number and name.
  296. .
  297. .TP
  298. .B -s
  299. Include all send operations in the output of simulation runs.
  300. .
  301. .TP
  302. .B -T
  303. Do not automatically indent the
  304. .I printf
  305. output of process
  306. .I i
  307. with
  308. .I i
  309. tabs.
  310. .
  311. .TP
  312. .B -t[\f2N\f1]
  313. Perform a guided simulation, following the [\f2N\f1th] error trail that
  314. was produces by an earlier verification run, see the online manuals
  315. for the details on verification. By default the error trail is looked for
  316. in a file with the same basename as the model, and with extension .trail.
  317. See also
  318. .BR -k .
  319. .
  320. .TP
  321. .B -v
  322. Verbose mode, add some more detail, and generate more
  323. hints and warnings about the model.
  324. .
  325. .TP
  326. .B -V
  327. Prints the
  328. .I spin
  329. version number and exit.
  330. .
  331. .PP
  332. With only a filename as an argument and no option flags,
  333. .I spin
  334. performs a random simulation of the model specified in
  335. the file.
  336. This normally does not generate output, except what is generated
  337. explicitly by the user within the model with
  338. .I printf
  339. statements, and some details about the final state that is
  340. reached after the simulation completes.
  341. The group of options
  342. .B -bgilmprstv
  343. is used to set the desired level of information that the user wants
  344. about a random, guided, or interactive simulation run.
  345. Every line of output normally contains a reference to the source
  346. line in the specification that generated it.
  347. If option
  348. .B -i
  349. is included, the simulation i
  350. .IR interactive ,
  351. or if option
  352. .B -t
  353. or
  354. .BI -k file
  355. is added, the simulation is
  356. .IR guided .
  357. .
  358. .SH SOURCE
  359. .B /sys/src/cmd/spin
  360. .SH SEE ALSO
  361. .in +4
  362. .ti -4
  363. .B http://spinroot.com/spin/Man/
  364. .br
  365. .in -4
  366. G.J. Holzmann,
  367. .IR "The Spin Model Checker (Primer and Reference Manual)" ,
  368. Addison-Wesley, Reading, Mass., 2004.
  369. .br
  370. —, `The model checker Spin,'
  371. .IR "IEEE Trans. on SE" ,
  372. Vol, 23, No. 5, May 1997.
  373. .br
  374. —, `Design and validation of protocols: a tutorial,'
  375. .IR "Computer Networks and ISDN Systems" ,
  376. Vol. 25, No. 9, 1993, pp. 981-1017.
  377. .br
  378. —,
  379. .IR "Design and Validation of Computer Protocols" ,
  380. Prentice Hall, Englewood Cliffs, NJ, 1991.