Spin Model Checker, The: Primer and Reference Manual

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