A forum for Spin users
You are not logged in.
I need to run a number of experiments, and so need to automatically detect when a never claim is violated. I am looking at two output files from pan, one for a run where a never claim is violated, and one where it is not (see below). There is no indication that I can see that I can parse automatically. Is there some switch I need to set to get such an indication? Is there some cue that I am overlooking?
Never claim satisfied:
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 1)
pan: wrote PROBLEM_X-spin.pml.trail
(Spin Version 6.1.0 -- 4 May 2011)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (never_0)
assertion violations + (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 1, errors: 1
1 states, stored
0 states, matched
1 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.228 actual memory usage for states (unsuccessful compression: 426728.57%)
state-vector as stored = 238940 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 secondsNever claim violated:
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 153)
pan: wrote P01_AIRPORT1_P1-spin.pml.trail
(Spin Version 6.1.0 -- 4 May 2011)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (never_0)
assertion violations + (if within scope of claim)
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 203, errors: 1
180 states, stored
13 states, matched
193 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.010 equivalent memory usage for states (stored*(State-vector + overhead))
0.272 actual memory usage for states (unsuccessful compression: 2832.98%)
state-vector as stored = 1558 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.01 secondsOffline
I think I had this wrong. I was actually having a race condition: the problem was that my never claim was starting before the variables were set to their initial values, so in the case where I thought it was not violated, it actually was trivially violated, since the variable in question was being checked for == 0.
I fixed this by setting the initial values in a d_step and adding a skip; at the start of the never claim.
I confess to not being certain why a single "skip;" is enough to ensure that the never claim doesn't "start too soon"....
Offline