How to use Spin to check Promela code from the command line

I'm looking how to analyse the output of train.pml using Spin on the Windows 10 command line.

Any help to make the file give the correct output would be greatly appreciated.

Solution

pre-requisites: get a working environment with gcc on Windows 10 (e.g. see these instructions) or, alternatively, get a virtual environment with some GNU/Linux distribution. Also, correctly install Spin in the target system.

There are only two possible approaches:

option A.:

~$ spin -a train.pml
~$ gcc pan.c -o verifier
~$ ./verifier -a -N c1
...
~$ ./verifier -a -N c8
...

option B.:

~$ spin -search -ltl c1 train.pml
...
~$ spin -search -ltl c8 train.pml
...

At the time being, properties c1, c5, c7, c8 are verified on your model, whereas c2, c3, c4, c6 are not verified. There are also some complaints about unreached end states. Please check that the latter condition does not violate the specification of your system (it may or may not be a problem), and that the outcome of the verification matches your expectation.

As a reference, this is an example of the correct output that you should obtain when verifying property c1:

~$ spin -search -a -ltl c1 trail.pml
...
pan: ltl formula c1

(Spin Version 6.4.6 -- 2 December 2016)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (c1)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 152 byte, depth reached 4508, errors: 0
    67919 states, stored (97586 visited)
   170919 states, matched
   268505 transitions (= visited+matched)
        0 atomic steps
hash conflicts:       184 (resolved)

Stats on memory usage (in Megabytes):
   11.659   equivalent memory usage for states (stored*(State-vector + overhead))
    5.455   actual memory usage for states (compression: 46.78%)
            state-vector as stored = 56 byte + 28 byte overhead
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  133.905   total actual memory usage


unreached in proctype train
    trail.pml:31, state 14, "-end-"
    (1 of 14 states)
unreached in proctype gate
    trail.pml:52, state 17, "-end-"
    (1 of 17 states)
unreached in proctype queue
    trail.pml:74, state 17, "-end-"
    (1 of 17 states)
unreached in claim c1
    _spin_nvr.tmp:10, state 13, "-end-"
    (1 of 13 states)

pan: elapsed time 0.12 seconds
pan: rate 813216.67 states/second