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

Hi Doron,


On Sun, Oct 28, 2007 at 10:47:31AM +0200, Bustan, Doron wrote:
> 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?

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

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

Johan

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

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