Hi Johan, I remember talking with John about the things that you mentioned on 2005... There were some e-mail exchange with Cindi and Dana, and I remember some new definition where \top satisfies every sequence. Maybe we can do something about that in the 2010 release. Doron >>-----Original Message----- >>From: Johan M?rtensson [mailto:johan.martensson@jasper-da.com] >>Sent: Thursday, December 06, 2007 1:04 PM >>To: Bustan, Doron >>Cc: sv-ac@eda.org >>Subject: Re: [sv-ac] informal definition of the weak operator >> >>Hi Doron, >> >>I like this kind of thing. Me, John, Dana Fisman and Cindy Eisner wrote >>a paper (unpublished and called "Truncating Regular Expressions") back >>in 2004 on what I think is a similar thing which we called the >>weak/strong word semantics. The purpose was to solve the embarrassing >>problem of structural contradictions in weakly embedded sequences and >>abort. >> >>For example >> >>if sc is the sequence (1 intersect (1[*2])) then >> >>*) weak(1[*0:$] ##1 sc) >> >>will not be satisfiable according to the current semantics. The problem >>is that sc will not match tightly on any word not even if all the >>letters are of the type \top. >> >>I think there is a sound intuition about weak embedding saying that * >>should be true on every trace regardless of what sc is, because we >>should not even have to consider what sc is because the 1[*0:$] prefix >>will never get contradicted. >> >>also for similar reasons >> >>accept_on(b) weak(1[*0:$] ##1 sc) >> >>will not be satisfiable according to the current semantics. >> >>The weak/strong word semantics defines partial match of sequences and >>properties on finite weak and strong words (defined in the paper) in a >>way that disregards the parts of the formulas that are not matched. >> >>One problem with the current \top, \bot semantics is that although it >>solves similar problems when sc is a boolean contradiction by allowing >>satisfaction of a boolean contradiction on a letter it doesn't do the >>same thing for structural contradictions. The root problem as I see it >>is that the \top,\bot semantics retains the requirement of tight match >>of the entire sequence, albeit on a word containing letters that will >>accept any boolean. >> >>Best Regards, >> >>Johan >> >> >>On Thu, Dec 06, 2007 at 09:36:41AM +0200, Bustan, Doron wrote: >>> 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. >>> >> >>-- >>------------------------------------------------------------ >>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 >>------------------------------------------------------------ --------------------------------------------------------------------- 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.Received on Thu Dec 6 04:02:39 2007
This archive was generated by hypermail 2.1.8 : Thu Dec 06 2007 - 04:03:05 PST