[sv-ac] weak operator

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.

 

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.

 

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.

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