Spin Model Checker, The: Primer and Reference Manual

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