Re: [sv-ac]16.14.8 Nonvacuous evaluations // question on accept/reject forms

OK, my error, the accept is an abort and the result is vacuously true
per 16.12.14
Abort properties
"For an evaluation of accept_on (expression_or_dist) property_expr and
of sync_accept_on (expression_or_dist) property_expr, there is an
evaluation of the underlying property_expr.* If during the evaluation, the
abort condition becomes true, then the overall evaluation of the property
results in true*. "
Ben Cohen

On Mon, Feb 6, 2012 at 3:31 PM, Ben Cohen <hdlcohen@gmail.com> wrote:

> LRM states: "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."
>
> But in reality, there is another condition where the evaluation attempt of
> a property of the form accept_on(expression_or_dist) property_expr is
> nonvacuous: Specifically *if expression_or_dist holds in any time step of
> that evaluation attempt, then the evaluation is nonvacuous true.*
> *Did we miss that case? *
> *
> *
> I have similar comments on the other properties with accept/reject
>
> Ben Cohen
>

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