Spinroot

A forum for Spin users

You are not logged in.

#1 2012-03-05 14:56:43

leduykhanh
Member
Registered: 2012-03-05
Posts: 2

[Solved] Error when verifying LTL property

Hi all,

I am having the following PROMELA program with a LTL property "pr" which should hold:

int x;

init { 
  x=1; 
  x=2;
  x=3;
  x=4;
}

ltl pr { [](x==1 -> <> x==3)}

However, when I verify this with SPIN, I got an an expected error as follow:

$ spin -a test2.pml
ltl pr: [] ((! ((x==1))) || ((328==3)))
$ gcc -o test2 pan.c
$ ./test2

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)
pan:1: end state in claim reached (at depth 5)
pan: wrote test2.pml.trail

(Spin Version 6.1.0 -- 4 May 2011)
Warning: Search not completed
	+ Partial Order Reduction

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

State-vector 28 byte, depth reached 5, errors: 1
        3 states, stored
        0 states, matched
        3 transitions (= stored+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: 181947.62%)
         	state-vector as stored = 101863 byte + 28 byte overhead
    4.000	memory used for hash table (-w19)
    0.534	memory used for DFS stack (-m10000)
    4.730	total actual memory usage


pan: elapsed time 0 seconds

The counter example in "test2.pml.trail" is as follow:

-2:1:-2
-4:-4:-4
1:0:7
2:1:0
3:0:5
4:1:1
5:0:11

Here are my concerns:

1) Why there is some weird number "328" when generating pan.c from test2.pml (that should be "x")
$ spin -a test2.pml
ltl pr: [] ((! ((x==1))) || ((328==3)))

2) Why there is an error? (this is a sequential program; therefore, I think the property "pr" holds)

3) I could not really understand what the counter example wants to express? (I don't mean the numbers, I re-run using ispin but I could not understand the counter-example)

Thank you so much for your help. Sorry if my question seems stupod 'cause I am just a newbie wink

Last edited by leduykhanh (2012-03-05 18:21:31)

Offline

#2 2012-03-05 16:54:03

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

Re: [Solved] Error when verifying LTL property

that's an interesting one
the problem is the precendence order of the operators.
you said: ltl pr { [](x==1 -> <> x==3)}
what you want: ltl pr { [](x==1 -> <> (x==3))}
the last clause in the version you gave is interpreted as (( <> x ) == 3)
which doesn't make much sense of course, and causes it to think "<> == 3" which produces that (328 == 3).
definitely unexpected!

Offline

#3 2012-03-05 18:21:14

leduykhanh
Member
Registered: 2012-03-05
Posts: 2

Re: [Solved] Error when verifying LTL property

Your help definitely solved my silly questions ^_^ Thank you so much.

Offline

#4 2012-05-20 17:49:58

amrad
Member
Registered: 2012-02-15
Posts: 4

Re: [Solved] Error when verifying LTL property

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.

Offline

#5 2012-05-20 18:47:19

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

Re: [Solved] Error when verifying LTL property

since you defined the ltl property inline, there is no need to generate it separately.
you can simply do:

spin -a random0.pml
cc -o pan pan.c
./pan

and you'll get:

$ spin -a try2.pml
ltl p1: [] ((p0==0))
$ cc -o pan pan.c
$ ./pan
warning: never claim + accept labels requires -a flag to fully verify
hint: this search is more efficient if pan.c is compiled -DSAFETY
pan:1: end state in claim reached (at depth 15)
pan: wrote try2.pml.trail

(Spin Version 6.2.2 -- 19 May 2012)
Warning: Search not completed
    + 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 28 byte, depth reached 15, errors: 1
        8 states, stored
        0 states, matched
        8 transitions (= stored+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.291    actual memory usage for states
  128.000    memory used for hash table (-w24)
    0.534    memory used for DFS stack (-m10000)
  128.730    total actual memory usage

pan: elapsed time 0 seconds

Offline

#6 2012-05-21 14:32:11

amrad
Member
Registered: 2012-02-15
Posts: 4

Re: [Solved] Error when verifying LTL property

Thanks a lot for your quick reply.

But i would like to know if the "errors: 1" in the message  means that the property is false?


thank you.

Last edited by amrad (2012-05-21 16:27:49)

Offline

#7 2012-05-21 16:37:05

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

Re: [Solved] Error when verifying LTL property

yes it does
you can replay the error trace with:
  spin -t -p -l -g -v random0.pml

Offline

#8 2012-05-29 08:45:17

memorialurn
Member
From: united states
Registered: 2012-05-29
Posts: 1
Website

Re: [Solved] Error when verifying LTL property

thanks...what is role of spin is here....

Offline

Board footer

Powered by FluxBB