Hi Johan, John, I corrected most of Johan's comments. There is only the one below. I think I understands this, but it would be good if John could say his opinion. >>F.3.1.1 Rewrite rules for sequences. >>==================================== >> >>"The transformation T^s(S,c) recursively defined below produces an >>unclocked sequence R equivalent to a given clocked sequence S with a >>leading clock c" >> >> Not all clocked sequences according to the abstract syntax (F.2.1) have >> a leading clock, for example (@(c1)R1)##1(@(c2)R2). However the clock >> rewrite rules are applicable also in this case by >> T^s((@(c1)R1)##1(@(c2)R2),1). [[DB:]] As far as I understand 16.15 and 16.15.1, in this case c1 is the leading clock. >> >> In addition according to the (Draft4) abstract syntax for the clocked >> sequence '@(c) R' R must be unclocked. To apply the rewrite to this >> clocked sequence would be to evaluate T^s(R,c) or to evaluate T^s(@(c) >> R,1). Neither of these seem to match with the description. >> [[DB:]] I think that T^s(R,c) does match the description. >> BTW. I hope we have some mantis item for removing the restriction that >> clocks cannot be nested in the abstract syntax. [[DB:]] I agree. I am not sure I know all the details that lead to this restriction. Maybe John knows. >> >>Maybe the following could serve as a replacement. >> >> "The transformation T^s(S,c) recursively defined below produces an >> unclocked sequence R equivalent to a given clocked (or unclocked) >> sequence S in the context of a clock c" >> >> [[DB:]] I think that for sequences this is not needed. I am not sure about properties of the form "@(c1)p1 or @(c2)p2" >>F.3.1.2 Rewrite rules for properties. >>==================================== >> >>Similar comment to that of F.3.1.1 >> Thanks 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 Wed Dec 5 06:23:04 2007
This archive was generated by hypermail 2.1.8 : Wed Dec 05 2007 - 06:23:36 PST