[sv-ac] Notes of false vacuity + NO Meeting on Tuesday

Dmitry,
Actually, I got that issue of simulation statistics and vacuous fail
 resolved thanks to your help. We don't need a meeting. Just for the
record, what is confusing in the LRM is the vacuity statements and the
true/false statements on the *not *and the *reject_on* operators. As we
often talked about,in our meeting, vacuity and true/false are separate
notions. Thus, the LRM infers the notion of "false vacuity", or fail
"vacuously" . For example:
  *not*( 0 |-> p) is both false and vacuous.
What confused me is my concept (or misconception?) that if a property is
vacuous, it is because it is not meaningful in terms of statistics, that is
is why it is vacuous. So when (*not*( 0 |-> p) ) contributes to the
statistics, it just feels odd, just from the definition of vacuity. If I
truly wanted a vacuous property to fail for the *not *and
*reject_on*operators, I envisioned something like the following
(assuming that
anything vacuous is not counted) :
    *not*( a |-> p) *and *a // If a==0, we get vacuous for (a |->p) ANDed
with a nonvacuous false.
    *reject_on*(a) p *and *!a[*] // if a==0, p gets evaluated. If a==1,
we get a vacuous (*reject_on*(a) p) ANDed with a nonvacuous false.

So, in essence, even though my reasoning sounded right (I think!) this is
not how it is (loosely I think) defined in the LRM. There is no point in
pushing it. However, In the next iteration of 1800, it might be worth to
clarify this notion of "false vacuity" because it does exist -- A property
 can be both: false (e.g., 16.12.2 Negation property) and vacuous
(e.g., 16.14.8
d), and it is not explicitly clear when a false vacuously is counted in the
statistics (can you point to the section for me?).

Ben Cohen

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.