## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

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.

No credit card required