What are the steps to verify LTL with SPIN tool?

4
votes

I wrote a model in Spin. I want to check some LTL on the model. for example:

ltl L1 {<>[]Working}

in the Verification window i choose option "use claim" and click "Run":

ltl L1: <> ([] (Working))
gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c

at this point I have no idea what to do next...? I've tried to look for the answer with Google but there are no guides how to use Spin....

2
spinpromela
Why is @Matte Schwerhoff 's answer not accepted ? – Ioannis Filippidis

2 Answers

3
votes

  1. Save your model including the ltl-block in foo.pml

  2. spin -a foo.pml

  3. gcc -o foo.exe pan.c (Windows)

  4. foo.exe -a

Running the executable with -a is the key, otherwise, the LTL-property won't be checked.

1
votes

In the 'verification' window after your click 'run' there should be a verification result. It looks like this (for example):

verification result:
spin -a  foo.pml
ltl ltl_0: [] (foo)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -o pan pan.c
./pan -m10000  -a -c1
Pid: 21462

(Spin Version 6.2.4 -- 21 November 2012)
    + Partial Order Reduction
...

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

Are you not seeing any of that? Or are you seeing something but can't interpret it?