A forum for Spin users
You are not logged in.
Pages: 1
Your help definitely solved my silly questions ^_^ Thank you so much.
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
Pages: 1