Re: [sv-ac] vacuity

Hi Dimitry,

I agree that the current definition may not give the user all the 
information he wants.
There are many different definitions of vacuity, most of them are far 
more reach than
the one we proposed.

Nevertheless, it is not clear that these definitions should be add to 
the LRM.
The downside of having more than one definition in the LRM is  that it 
overloads
the reports requirements. You will expect a tool that is LRM compliant 
to able
to report the successes according to each type of vacuity, it will 
create a substantial
overhead.

The advantage of the current proposal, is by its locality. Meaning, the 
non-vacuity
is determined per attempt and ignores other attempts. This allows a 
simple report, and
a simple decision procedure for the execution of action blocks.

As for your proposal:

> * For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$
> iff
>      $w,L \non P_1$ and $w,L\non P_2$.
> 
>  * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$
> iff
>      $w,L \non P_1$ and $w,L\non P_2$.


I think it is too strict, because  some properties P1 and P2 cannot 
succeed non vacuously
at the same attempt.

For example for the derived operator

$if (b) P1 else P2 \equive (b |-> P1) and (!b |-> P2)$

there are no attempts in which both $(b |-> P1) $ and $(!b |-> P2)$
hold non-vacuously.

regards

Doron



Korchemny, Dmitry wrote:

>Hi Doron,
>
>I agree with your proposal what the "top level" vacuity is concerned. If
>I understood it correctly, it essentially says that the vacuity is
>defined according to the top level binary operator; I am ignoring the
>reset issue for the sake of simplicity. To be more accurate, if the
>antecedent of the property in the implication normal form never matches,
>and the property passes, it passes vacuously.
>
>Nevertheless the user is often interested to get the partial vacuity
>data as well. Consider the following example:
>
>assert property ((a |-> b) and (c |-> d));
>
>Suppose that a happens in the input word, but c never happens. According
>to your definition the property passes non-vacuously, but the
>information about the partial vacuity is also important. We need to
>define some discrimination mechanism which will enable the exact
>reporting. One option is to enumerate the implication operators inside a
>property in a lexicographical order.
>
>E.g., the reporting might be that the second implication executed
>vacuously.
>
>Therefore I am suggesting defining to kinds of vacuity - global vacuity
>(= your definition) and partial vacuity (your definition with
>appropriate modifications for or and and):
>
>* For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$
>iff
>     $w,L \non P_1$ and $w,L\non P_2$.
>
> * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$
>iff
>     $w,L \non P_1$ and $w,L\non P_2$.
>
>What do you think?
>
>Dmitry
>
>-----Original Message-----
>From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
>Doron Bustan
>Sent: Tuesday, April 11, 2006 1:00 AM
>To: sv-ac@eda.org
>Subject: [sv-ac] vacuity
>
>I upload a new definition for vacuity.
>The new definition differ from the old
>one, at the "disable iff" operator.
>
>Doron
>  
>