RE: [sv-ac] When does an assertion fail vacuously?

Hi Ben,

Section 16.15.8 starts with:
“An evaluation attempt of a property is either vacuous or nonvacuous. In the following, nonvacuous
evaluation is described …”

and ends with
“An evaluation attempt of a property succeeds nonvacuously if, and only if, the property evaluates to true and
the evaluation attempt is nonvacuous.”

So yes, it does not explicitly say that
“An evaluation attempt of a property fails nonvacuously if, and only if, the property evaluates to false and
the evaluation attempt is nonvacuous.”

And yes, the property not (a |-> b) should fail vacuously if a never holds.

Regarding, accept_on (b) \phi – suppose that b never occurs and \phi fails vacuously, then the whole property fails, and according to item ab)
“An evaluation attempt of a property of the form accept_on(expression_or_dist) property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous and
expression_or_dist does not hold in any time step of that evaluation attempt.”
it is vacuous.

Best,
Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Wednesday, October 06, 2010 5:12 AM
To: sv-ac@eda.org; Korchemny, Dmitry
Subject: [sv-ac] When does an assertion fail vacuously?

Where is vacuous fail defined in the LRM? I could not find it.
Consider the property (not (a |-> b)), and "a"==0; Then (a|-> b) is vacuous success.
Does that mean that not(a|->b) is vacuous fail?
Also, at our meeting today, I heard that accept_on can produce vacuous fail. I don't get it.
Can you point me to cases of vacuous failure, and where in the LRM this defintion exists?

16.15.8 defines nonvacuous, but the LRM does not define vacuous (I don’t think).
I can't find vacuous fail or vacuous pass. It can succeed vacuously, but that is not a pass or a fail.
Also, here is a pass counter, fail counter, vacuous counter.

Thanks,
Ben

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.