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.


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

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

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.