Chapter 15. Sample SPIN Models


“Few things are harder to put up with than the annoyance of a good example.”

 --(Mark Twain, 1835–1910)

In this chapter we will discuss a few small PROMELA models that exploit some interesting and possibly useful features of the specification language. We will focus mostly on language and modeling issues here. More examples of PROMELA models can be found in the standard SPIN distribution.


Our first example is a PROMELA version of an ancient algorithm for finding primes by counting off numbers and systematically intercepting the non-primes among them. The algorithm, a favorite programming exercise today, is due to the Greek philosopher and mathematician Eratosthenes of Cyrene (a city in modern day Libya ...

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.