Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-14 13:20:00

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Model pan.c cannot compile with both embedded LTL and -DNP cflag

init {
  skip;
}

ltl p1 { [](true) };
ltl p2 { [](true) };

In file included from pan.c:30:
pan.h:205: error: "NCLAIMS" undeclared here (not in a function)
make: *** [test1] Error 1

Is it a bug?

Offline

#2 2011-02-17 01:27:05

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

I cannot reproduce this problem -- which version of Spin did you use for this?
With the current version (6.0.2 or 6.0.1) it compiles correctly.

Offline

#3 2011-02-17 01:41:43

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

I am using 6.0.1 with
spin -a -q test.spn && gcc -O2 -DNP pan.c -o pan

Weird you cannot reproduce it...

Offline

#4 2011-02-17 01:48:32

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

Here's what I get when I run it -- but there's a key difference I see: you used -DNP.
I do see the same error when I add -DNP. I'll check it out.

$ spin -a -q abug.pml
ltl p1: [] (1)
ltl p2: [] (1)
  the model contains 2 never claims: p2, p1
  only one claim is used in a verification run
  choose which one with ./pan -N name (defaults to -N p1)

[email protected] ~
$ cc -o pan pan.c

[email protected] ~
$ ./pan
warning: never claim + accept labels requires -a flag to fully verify
hint: this search is more efficient if pan.c is compiled -DSAFETY
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
0: Claim p1 (1), from state 5

(Spin Version 6.0.2 -- 22 January 2011)
        + Partial Order Reduction

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

State-vector 20 byte, depth reached 5, errors: 0
        3 states, stored
        1 states, matched
        4 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

    2.501       memory usage (Mbyte)

unreached in init
        (0 of 2 states)
unreached in claim p1
        _spin_nvr.tmp:8, state 8, "-end-"
        (1 of 8 states)
unreached in claim p2
        _spin_nvr.tmp:17, state 8, "-end-"
        (1 of 8 states)

pan: elapsed time 0.003 seconds

Offline

#5 2011-02-17 01:50:43

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

OK, thanks. BTW is SPIN 6.0.2 publicly available now?

Offline

#6 2011-02-17 05:03:03

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

This is indeed a bug in 6.0.1 -- it will be fixed in 6.0.2.
This version isn't on the website yet, but I'll probably add it in another week or so.
Thanks for reporting this bug!

Offline

#7 2011-02-17 05:35:45

jiong
Member
From: China
Registered: 2011-01-27
Posts: 30

Re: Model pan.c cannot compile with both embedded LTL and -DNP cflag

Great! Thanks, Gerard! I am looking forward to the new version out!

Offline

Board footer

Powered by FluxBB