RE: [sv-ac] vacuity

Hello John,
regarding
 "b" in "disable iff (b) P", it does not affect "\non".
But what if \non P holds only if you include the times when the disable
condition is true and actually the property is disabled? Will you not
get an optimistic result? 

ed


> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of John Havlicek
> Sent: Thursday, March 30, 2006 3:26 PM
> To: dbustan@freescale.com
> Cc: sv-ac@eda.org
> Subject: Re: [sv-ac] vacuity
> 
> All:
> 
> Note that "\non" is a relation that defines when an evaluation
> is non-vacuous.  "w,L \non P" does not imply "w,L |= P", so that 
> "\non" does not say anything about whether the evaluation results
> in success or failure.
> 
> The definition of "pass non-vacuously" would then be "w,L |= P" 
> and "w,L \non P".
> 
> Regarding "b" in "disable iff (b) P", it does not affect "\non".
> 
> Also, note that if we had followed_by, we would get
> 
>    w,L \non R followed_by P
>    iff  w,L \non not(R |-> not P)
>    iff  w,L \non R |-> not P
>    iff  w,L \non R |-> P
> 
> Best regards,
> 
> John H.
> 
> 
> > Here is an attempt to define when an assertion pass non-vacuously.
> > This proposal is also available at mentis (1381).
> > This is not a proposal, it's a definition for review and discussion.
> > 
> > There are a lot of vacuity definitions, I tried to have a 
> simple definition
> > that generalizes the implication vacuity that is already 
> being used. The
> > definition is on the structure of the property, on the 
> property level, 
> > meaning
> > we have a new satisfaction relation. Let $\tight$ be the 
> tight satisfaction
> > relation, $\models$ the satisfaction relation and $\non$ the
> > non-vacuous  relation. An attempt of a property $P$ on a suffix $w$
> > pass non vacuously iff $w,{}\models P$ and $w,{}\non P$.
> > 
> > The definition of $\non$ is per attempt on a suffix $w$ of 
> a computation.
> > 
> > Base: For every sequence $R$, property $P=R$, and 
> assignment $L$, we 
> > have that          
> > $w,L\non P$.
> > 
> > Induction:
> > 
> >  * For $P =  (P_1)$ and assignment $L$, we have that 
> $w,L\non P$  iff
> >      $w,L \non P_1$.
> > 
> >  * For $P = R |-> P_1$ and assignment $L$, we have that 
> $w,L\non P$  iff
> >      there exists $i \geq 0$, and an assignment $L_1$ such that
> >      $w^{0..i}, {}, L_1 \tight R$ and $w^{i..}, L_1\non P_1$.
> > 
> >  * For $P = P_1 and P_2$ and assignment $L$, we have that 
> $w,L\non P$  iff
> >      $w,L \non P_1$ or $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$ or $w,L\non P_2$.
> > 
> >  * For $P = not P_1$ and assignment $L$, we have that 
> $w,L\non P$  iff
> >      $w,L \non P_1$.
> > 
> >  * For $P = disable iff (b) P_1$ and assignment $L$, we have that 
> > $w,L\non P$  iff
> >      $w,L \non P_1$.
> > 
> > 
> > 
>