RE: [sv-ac] 1932 Questions on non vacuity.

Hi Johan,

I agree that this definition is not always intuitive. However, 
it is not part of 1932 and I would not like to tie the existing vacuity 
definition to 1932.

1. The principles that guided me when I wrote this definition were 
   as follows:

2. It should be backward compatible with the "old" definition which      
   considered only implications. 

3. It is better to have unintuitive 
   non-vacuous successes than unintuitive lack of non vacuous successes. 
   This is because I consider vacuity checking as automatic extraction of 
   cover goals. I consider these extracted properties as a bonus, but a   
   cover property that should not be cover is a noise.

4. The judgment whether there is a witness for non vacuity for a property in 
   a model is made per attempt. In other words from every property there 
   going to be at most one extracted cover property. I think this create the 
   problem with your example because what we need are two cover properties 
   "a ##1 b" and "c ##1 d" but these properties may be hit on different 
   attempts in different simulation runs. 

5. Another principle that we didn't fully achieve is that checking for  
   vacuity should be "for free" as a by product of checking the assertion.


There are much more intuitive definitions in the literature. However, I think that all of them conflict with principles 4 and 5. We should consider what we want but I suspect we will not change the basic concept for the 2008 release.

I would go for something close to definition of

R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, and M. Vardi. 
Enhanced vacuity detection in linear temporal logic. 
In Computer Aided Verfication, 15th Inte.l Conf., (CAV 2003), volume 2725 of LNCS, pages 368–380, 2003.

Doron


-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Johan M?rtensson
Sent: Wednesday, October 24, 2007 11:35 AM
To: Bustan, Doron; John Havlicek
Cc: sv-ac@server.eda.org
Subject: Re: [sv-ac] 1932 Questions on non vacuity.

Hi Doron, John,

I have some questions on the non-vacutity definition. It is stated that
a word w satisfies a property P non-vacuosly iff w|= P and w|=non P.

1) I think the clause that for every sequence R 'w|=non R' may give rise
to some unintuitive consequences.

For example consider the property P=(a|->b or c|->d). A trace w where
w|=a, w|/=b and w|/=c will satisfy P non-vacuosly although the only
disjunct of P that is satisfied by w is satisfied vacuously.

 w|/= a|->b
 w|= c|->d
so
 w|= a|->b or c|->d

 w|=non a|->b [because w^{0..0}|-a and w|=non b]
 w|/=non c|->d
so
 w|=non a|->b or c|->d

2) I suspect that the clause
  w|=non not P <=> w|=non P can create trouble in a similar way.

3) The clause for until looks strange to me. Why do we require that one
of the operands is satisfied non vacuously in the first cycle
specifially? If only once Why not on some later cycle instead?

4) The case for and only requires that one of the operands satisfy
non-vacously. Is this sufficient?

However I think it is very important to be able to present sanity traces
that users find useful, so I think this effort is worthwile.

I have been experimenting with the following transformation to compute
non vacuous finite traces for proven safety properties.

(This definition is a shot in the dark and it doesn't seem to carry over
nicely into the non-safety domain, but it gives nice informative sanity
traces in many cases.)

N(a) = a
N(weak(r)) = strong(r)
N(P1 or P2) = N(P1) or N(P2)
N(P1 and P2) = N(P1) and N(P2)
N(X P) = X! N(P)
N(X! P) = X N(P)
N(P1 until P2) = (not P2) s_until_with N(P1)
N(r |=> P) = r #=# N(P)

If P is safety then N(P) is co-safety so if w|= N(P) then there is
finite prefix u of w such that u|=+ N(P) (u strongly satisfies N(P).

The idea is to ask the tool to look for a finite trace w such that w|=+
N(P') where P' is P with all negations pushed to the leaves. If there is
such a trace then this trace is presented to the user as a non-vacuous
witness of the property.

Best Regards,

Johan


-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.