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

Hi Doron,

some comments



On Thu, Oct 25, 2007 at 09:06:38AM +0200, Bustan, Doron wrote:
> 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.

Ok I agree. If we are going to revise the non-vacuity definition not
only for the new operators it should be a separate mantis item.

> 
> 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.

I agree, but sometimes there may be too much noise. Consider the
following

For all P it is the case that

w|=non always P

 
 w|=non always P
<=> [1932: F.2.3.2.7]
 w|=non P until 0
<=> [1932: 16.12.1]
 w|=non P until weak(0)
<=> [1932: F.3.3.3]
 w|=non P or w|=non weak(0)
<= [1932: F.3.3.3: w|= non weak(0)]
 true

Is this the intention?


> 
> 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. 

The rewrite I suggested will give you the formula 'a #-# b or c #-# d'
for the original formula 'a|->b or c|->d'

 N(a|->b or c|->d) 
=
 N(a|->b) or N(c|->d) 
=
 a #-# N(b) or c #-# N(d) 
=
 a #-# b or c #-# d 

The trace w in the example will then come out as vacuous since although
w|= a|->b or c|->d, it is the case that w|/= a #-# b or c #-# d.


> 
> 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.

In the article the problem of determining which subformulas of a formula
F true of a model M are non-affecting in that formula w.r.t. M. How is this
related to the problem at hand?

We are trying to define a relation of non-vacuity between traces and
formulas. How exactly is this problem related to the problem of
subformula vacuity w.r.t. to models discussed in the article?

I can see some connections but I am not sure about the details. For
example even in a situation where the formula F has non-affecting
subformulas w.r.t. the model M we may want to compute a non vacuous
trace for F, and in fact the current definition does. Consider the
formula 'p|->p'.  The subformula p is not affecting for any M.
Nevertheless if w^0|-p then w|=non p|->p.

Best Regards,

Johan

> 
> 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.

-- 
------------------------------------------------------------
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.