A forum for Spin users
You are not logged in.
Pages: 1
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
Last edited by leduykhanh (2012-03-05 18:21:31)
Offline
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
Your help definitely solved my silly questions ^_^ Thank you so much.
Offline
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
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
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
thanks...what is role of spin is here....
Offline
Pages: 1