Spin

Citations

Homepage

github

Spin verification examples and exercises

Simulation run

spin -uN -v -p model.pml

-v for verbose, -p for printing all statements, -uN for stopping the simulation run after N steps.

Verification run

spin -run -mN model.pml

-mN for limiting the number of steps in the verification at N. N defaults to 10,000.

Replay the error trail file

spin -replay model.pml

ProMeLa

Predefined variables

_pid for the process id. _nr_pr for the number of active prosess, max 255.