A forum for Spin users
You are not logged in.
Pages: 1
Hello spinroot,
I have the following program, where []a should hold:
bit p;
init
{
p = 1;
}
#define a p
active proctype test()
{
d_step { p = 1;}
do
:: p -> goto accept
od;
accept: printf("Accepted");
}
never { /* !([](a)) */
T0_init:
if
:: (! ((a))) -> goto accept_all
:: (1) -> goto T0_init
fi;
accept_all:
skip
}
But there is an error:
$ spin -a source.pml
$ gcc -o pan pan.c
$ ./pan -m2000 -x -a
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 3)
pan: wrote source.pml.trail
(Spin Version 6.1.0 -- 2 May 2011)
Warning: Search not completed
+ 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 36 byte, depth reached 3, errors: 1
2 states, stored
0 states, matched
2 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 (unsuccessful compression: 238334.38%)
state-vector as stored = 152506 byte + 28 byte overhead
4.000 memory used for hash table (-w19)
0.107 memory used for DFS stack (-m2000)
4.302 total actual memory usage
pan: elapsed time 0 seconds
$ spin -t -p source.pml
Never claim moves to line 23 [(!(p))]
2: proc 1 (test) source.pml:12 (state 2) [p = 1]
Never claim moves to line 27 [(1)]
spin: trail ends after 3 steps
#processes: 2
p = 1
3: proc 1 (test) source.pml:13 (state 5)
3: proc 0 (:init:) source.pml:5 (state 1)
3: proc - (never_0) source.pml:28 (state 8) <valid end state>
2 processes created
I don't understand the following lines.
...
Never claim moves to line 23 [(!(p))]
2: proc 1 (test) source.pml:12 (state 2) [p = 1]
Never claim moves to line 27 [(1)]
...
Never claim searches for p=0 , but it is always p=1. Why does never claim move to line 27 [(1)]?
(Actually in line 27 there is "skip" and not (1) ).
What am I doing wrong?
Thanks!
Last edited by alb012 (2012-05-12 23:39:38)
Offline
Pages: 1