Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-25 16:24:08

rpg
Member
Registered: 2012-04-25
Posts: 2

Programmatically detect never claim violation in spin (pan) output

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 seconds

Never 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 seconds

Offline

#2 2012-04-25 17:18:25

rpg
Member
Registered: 2012-04-25
Posts: 2

Re: Programmatically detect never claim violation in spin (pan) output

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

Board footer

Powered by FluxBB