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

Hi Johan

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

[DB] The current status is that non-vacuity for until, and its derived
forms always/eventually ... will not be defined for the reasons you
specified above.


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

[DB] I have not study your proposal yet, but I have 2 comments.

The first is N(weak(r)) = strong(r), consider the property 
"weak(a[*1:$] ##1 0)" which is equivalent to "always a". Making the
Sequence strong makes the property a contradiction.

The second is that you need to add a definition for #=# and s_until_with
(the dual of until). Since you push "not" to the leaves you cannot use
the derived forms. For #-# the solution looks obvious "N(r #-# p) = r
#-# N(p)" but what about the strong until?


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

The idea is that for every sub property p' of p create a cover property
that witnesses that p' influences p. This is not compliant with the
non-vacuous relation but for every property that never pass
non-vacuously according to the current definition we will have a cover
property that is not covered. 
Such cover properties have a potential to flush many more problems, and
your example of r->r is one of them. I would like to know that one of my
sub properties is a tautology, because it probably not my intent (unless
I wrote "1"). 

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