[sv-ac] informal definition of the weak operator

Hi,

 

I just remembered that in 921 we have a definition of a weak match. This


definition is formal and does match the current definition for sequences
with  intersect (and its derived operators 

"and", "within", "throughout".) For infinite words we need to say that
it shall match every prefix. So, there are 

several reasons not to add it to 1932. Nevertheless, it adds intuition
to a confusing definition, and thus maybe it worth it.

(In my opinion this is a better definition then the current one.)

The definition is inductive: ||= is the new defined relation, |== is
tight satisfaction.

 

*      w,L0||= b iff either |w|=0 or |w|=1 and w |= b

*      w,L0||= (1,v=e) iff either |w|<=1 

*      w.L0||= R[*0] iff |w| = 0 

*      w.L0||= ( R ) iff w,L0 ||= R 

*      w.L0||= R1 or R2 iff w,L0 ||= R1 or w,L0 ||= R2

*      w.L0||= R1 intersect R2 iff w,L0 ||= R1 and w,L0 ||= R2

*      w.L0||= R1 ##1 R2 iff either w,L0 ||= R1 or for some xy=w and L1,
x,L0,L1|== R1 and ,y,L1 ||= R2

*      w.L0||= R1 ##0 R2 iff either for some y, |y|>0 wy,L0 ||= R1 or
for some xyz=w and L1, |y| = 1,  xy,L0,L1|== R1 and ,yz,L1 ||= R2

*      w.L0||= first_match(R1) iff w.L0||= R1 and for every xy=w and L1,
if |y|> 0 then x,L0,L1 |/== R1 

*      w.L0||= R1[*1:$] iff for some xy=w and L1, x,L0,L1 |== R1[*0:$],
and y,L1||= R1

 

Do you think it worth adding this definition somehow to the discussion?

 

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.