[sv-ac] Re: weak operator

Hi Doron,


On Wed, Dec 05, 2007 at 09:13:25AM +0200, Bustan, Doron wrote:
> Hi Johan,
> 
>  
> 
> I looked at the psl description:
> 
>  
> 
> * The FL property S holds on a given path iff either there exists a
> prefix of the path on which S holds tightly, or the given
> 
> path exhibits no evidence that the property S! does not hold on it.
> 

I think this is at best foggy at worst incorrect. I think it should be
changed to something like

* The FL property S holds on a given path iff either there exists a
prefix of the path on which S holds tightly, or no prefix of the given
path exhibits evidence that the property S! does not hold on it.



>  
> 
> NOTE-If S contains no contradictions, an easier description of the
> semantics of the property S can be given as follows: The
> 
> FL property S holds on a given path iff either there exists a prefix of
> the path on which S holds tightly, or the given path can
> 
> be extended to a path on which S holds tightly.
> 
>  
> 
> The additional description does not hold for infinite words. For example
> "weak(a[*0:$] ##1 b)" holds on 
> 
> an infinite word where "a" is always high and "b" is always low, but it
> is not clear which extension strongly 
> 
> match the sequence.

Yes that explanation is incorrect. I think It should be changed to
something like the following:

The FL property S holds on a given path iff either there exists a prefix
of the path on which S holds tightly, or every prefix of the given path
can be extended to a path on which S holds tightly.

I will notify the PSL committee of this.


Best Regards,

Johan


> 
>  
> 
> Doron
> 
>  
> 
>  
> 
>  
> 
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
> 
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Kvarnbergsgatan 2                Fax: +46 31 7451914
411 05 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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