O'Reilly logo

Spin Model Checker, The: Primer and Reference Manual by Gerard J. Holzmann

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required