4

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....

GoZoner
  • 67,920
  • 20
  • 95
  • 145
Junior Fasco
  • 227
  • 2
  • 11
  • 1
    Why is @Matte Schwerhoff 's [answer](http://stackoverflow.com/a/17209457/1959808) not accepted ? – 0 _ Jul 08 '14 at 17:26

2 Answers2

3

  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.

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
  • Hey, there should be an option to compile it from spin itself.. but for some reason Spin does not recognize my C compiler.. even though I changed the "environment varibels". – Junior Fasco Jun 20 '13 at 17:05
  • @JuniorFasco What do you mean by "compile it from spin itself"? – Malte Schwerhoff Jun 21 '13 at 07:00
  • @JuniorFasco there does exist now a [`-run` option](http://spinroot.com/spin/Man/Spin.html) to tell `spin` to call `gcc` and run the produced `pan`. Note that this option is new, nothing similar existed in the past. – 0 _ Jul 08 '14 at 17:29
1

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?

GoZoner
  • 67,920
  • 20
  • 95
  • 145