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.