Spinroot

Hi all,

i'm using Spin to verify some ltl property. i have the follwing promela programm with the hold ltl property:
int    p7,  p3,  p2,  p1,  p0;
init{
        p0 = 0 ;
    p3 = 2 ;
    p2 = 4 ;
    p1 = 1 ;
    p2 = 2 ;
    p0 = 4 ;
    p7 = 2 ;
    p7 = 0 ;
    p7 = 3 ;
    p7 = 1 ;
    p2 = 0 ;
        p0 = 0;
}
  ltl p1{ [] (p0 ==0 )}

To verify this property i have done thes instructions:
1- spin -f ' [] (p0 ==0 ) ' > buechi
2- spin -a -N buechi random0.pml
3- gcc -o pan pan.c
4- ./pan -a -n
However, when I verify this with SPIN, I got this message as follow:

(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.1.0 -- 4 May 2011)
    + Partial Order Reduction

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

State-vector 20 byte, depth reached 12, errors: 0
        7 states, stored (14 visited)
        5 states, matched
       19 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000    equivalent memory usage for states (stored*(State-vector + overhead))
    0.292    actual memory usage for states (unsuccessful compression: 121347.62%)
             state-vector as stored = 43669 byte + 16 byte overhead
    2.000    memory used for hash table (-w19)
    0.343    memory used for DFS stack (-m10000)
    2.539    total actual memory usage

pan: elapsed time 0 seconds

Can you please tell me what means this message. and is it true or false?

how can i know if this property is true or false?

thank to give us the clear and the best response.