Hi Johan, Ok, I am convinced that my text is bad (even wrong.) >"Similarly properties of the form weak(sequence_expr) are evaluated to >true if and only if the corresponding properties of the form >(weak(first_match(sequence_expr))) are evaluated to true >respectively. The reason is that a finite prefix of a trace vitnesses >a non-match of a sequence_expr if and only if it vitnesses a non-match >of the first_match of that sequence_expr." I don't think that the explanation adds any information to the reader. I don't see how to give informal explanation for the weak operator that is not confusing. Even the "finite witness" is wage. The "potential match" is wrong because sequences of the form "1[0:$] ##1 0" do not have potential matches, nevertheless "weak(1[0:$] ##1 0)" is a tautology. Maybe I will just put a note stating the equivalency between the sequences and first match. It does give some intuition 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.Received on Mon Dec 3 03:52:17 2007
This archive was generated by hypermail 2.1.8 : Mon Dec 03 2007 - 03:52:28 PST