Command Line Usage
------------------

Show options:

$ spin --help

Simulate verbose (-v) and show values of global vars (-g) for 100
steps (-u100):

$ spin -u100 -v -g counter.pml

Simulate along a trail file:

$ spin -v -g -k counter.pml.trail counter.pml

Create "protocol analyzer" (model-checker for counter.pml) pan.c:

$ spin -a counter.pml

Compile using gcc and run (default a.out):

$ gcc pan.c

Run analyzer (-a for analyze) for particular LTL property (-N liveness):

$ ./a.out -a -N liveness