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

Eratosthenes

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

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