A forum for Spin users
You are not logged in.
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
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
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)
gh@LARS01 ~
$ cc -o pan pan.c
gh@LARS01 ~
$ ./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
OK, thanks. BTW is SPIN 6.0.2 publicly available now?
Offline
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
Great! Thanks, Gerard! I am looking forward to the new version out!
Offline