Re: [sv-ac] vacuity

Hi Ed,

I talked with John, and we agree that there is a problem
with the disable iff.

I guess that we need to decide whether we want the "disabled" definition
to be defined independently, or whether the "disabled computations" should
be contained in the vacuous computations.

A definition for a relation $not_disable$ should be:

$w,L\not_disable disable iff (b) P$ iff for some prefix $x \leq w$, we 
have that
for every $0 \leq i < |x|$, $x^i \not\models b$, and either $x\cdot 
\bot^\omega,L \models P$
or $x\cdot \top^\omega,L \not\models P$.

meaning the "decision" whether  $P$ failed or succeed, occurs before the 
first occurrence of $b$

Then, we can define:

For $P = disable iff (b) P_1$ and assignment $L$, we have that 
$w,L\non P$  iff
     $w,L \non P_1$ and $w,L\not_disable P$.

Doron






Eduard Cerny wrote:

>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$.
>>>
>>>
>>>
>>>      
>>>
>
>  
>