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

Appendix C. Exercises With SPIN

 

“I hear and I forget; I see and I remember; I do and I understand.”

 
 --(Confucius, 551–479 BC)

C.1.

How many reachable states do you predict the following PROMELA model will generate?

init { /* example ex1 */
       byte i = 0;
       do
       :: i = i+1
       od
}

Try a simulation run:

$ spin -p -l -u100 ex1

Will the simulation terminate if the -u100 argument is omitted? Try it.

C.2.

Estimate the total number of reachable states that should be inspected in an exhaustive verification run. Is it a finite number? Will a verification run terminate? Try it as follows, and explain the result.

$ spin -a ex1
$ cc -o pan pan.c
$ ./pan

C.3.

What would happen if you had declared local variable i to be a short or an int instead of a byte?

C.4.

Predict accurately ...

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