Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » [Solved] Error when verifying LTL property » 2012-03-05 18:21:14

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

#2 General » [Solved] Error when verifying LTL property » 2012-03-05 14:56:43

leduykhanh
Replies: 7

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

Board footer

Powered by FluxBB