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

Hi Johan,

>> >> 
>> >> [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.
>> >
>> >I think it is hard to get a definition that will give the same
result
>> >for all equivalent formulas. Consider for example the pair 'a|->b'
and
>> >'!b|->!a'. I guess, a|->b should be non vacuous for a trace where a
and
>> >b are always true, but what about the second one?
>> 
>> [DB:] the point here is that there is a ligit weak sequence that will
>> never pass non vacuously. That will add noise.
>
>I thought that would reduce noice?
>
[DB] I consider this as a cover property that cannot be cover. So you
get a message of an uncovered cover goal, which is a false negative.

>> 
>> 
>> >> 
>> >> 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?
>> >> 
>> >
>> >Actually the transformation that I use is defined for strong
operators
>> >too:
>> >
>> >N(a) = a
>> >N(not P) = not N(p)
>> >N(weak(r)) = strong(r)
>> >N(strong(r)) = weak(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(P1 s_until P2) = N(P2) until_with (not P1)
>There is an error in the case for s_until.
>Should be:
>N(P1 s_until P2) = N(P2) until ((not P2) and not P1)
>See below
>> >N(r |-> P) = r #-# N(P)
>> >N(r |=> P) = r #=# N(P)
>> >
>> >
>> >If P is safety then N(P) is co-safety so if true, N(P) has a finite
>> >witness trace w (i.e. w is such that w|=+ N(P)).
>> >
>> >It gives pretty intuitive results for many safety properties. For
non
>> >safety the results are often weird though.
>> 
>> [DB:]I don't understand the definition for s_until???
>
>The transformation was written to work with safety properties. If we
>define
>
>P1 until_with P2 as (P1 until (P1 and P2))
>P1 s_until P2 as (not ((not P2) until (not P1))
>P1 s_until_with P2 as (P1 s_until (P1 and P2))
>
>Then we don't need cases for s_until and s_until_with. If we compute N
>for those cases they turn out to be
>
>N(P1 s_until P2) = N(P2) until ((not P2) and (not P1))
>N(P1 s_until_with P2) = N(P2) until (not P1)
>
>This of course gives unintuitive results for some non-safety properties
>using these operators. For example:
>
> N(s_eventually P)
>= [def s_eventually]
> N(T s_until P)
>=
> N(P) until ((not P) and (not T))
>=
> N(P) until ((not P) and F)
>
>so s_eventually P is non vacuously true on w only if P is always non
>vacuously true on w.
>
>This is the dual of the (desideratum) that 
>
>always P is non-vacuously true on w only if P is non-vacuously true at
some
>cycle of w.

[DB]: Here again I think that it will add noise. When I specify
"eventually p" I do not necessarily expect "always p" to hold in any
computation. So again you will get uncovered cover goal, which are false
negatives.



>
>> 
>> BTW, note that is possible that w satisfies N(P) but not P. For
example
>> "a[*1:2] |-> b" suppose that w has a prefix where a is high in the
first
>> two
>> cycles and b is high only at the first. Then w|= N(a[*1:2] |-> b) =
>> "a[*1:2] #-# b" but w |/= " a[*1:2] |-> b".
>
>It is indeed possible that w|=N(P) but not w|=P. This is also the case
>with |=non. The intention was to define non vacuous satisfaction as
w|=P >and w|=N(P).

Best regards

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.