Chapter 18. Overview of SPIN Options


“An error does not become a mistake unless you refuse to correct it.”

 --(Manfred Eigen, 1927–)

In this chapter we discuss all available SPIN options. The options are grouped into seven categories according to their primary use, as follows:

  • Compile-time options, which can be used to compile the SPIN source itself for different platforms and for different types of use

  • Simulation options, which can be used for customizing simulation runs of PROMELA models

  • Syntax checking options, for performing a basic check of the syntactic correctness of PROMELA models

  • LTL conversion options, describing various ways in which the conversion from LTL formulae to PROMELA never claims can be done

  • Model checker generation options

  • Postscript ...

Get Spin Model Checker, The: Primer and Reference Manual now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.