Hi, I resend this since it seems it wasn't reflected by the reflector :-). /Johan On Wed, Dec 05, 2007 at 11:20:51AM +0100, Johan Mårtensson wrote: Hi, I went through all of LTL_Formal.071120.pdf and here is my comments: F.2.1. ===== The abstract grammar for clocked properties. Instead of '|->' there is the sequence of symbols longdash-shortdash-upsidedownquestionmark. This is the case in for example F.3.3.1. F.2.3.1.4 Other derived operators ================================= In the case for throughout there is a 'b1' on the right hand side. It should be 'b'. F.2.3.2.1 Derived sequential property ===================================== I think the first occurrence of 'under' should be changed to 'in a' and the second one to 'in an'. F.2.3.2.4 Derived conditional operator ====================================== The rightmost P_1 should be changed to P_2. F.2.3.2.7 Derived unbounded temporal operators =============================================== In the case for s_until I think s_eventually and not eventually should be used on the right hand side. F.2.3.2.8 Derived bounded temporal operators ============================================ 1) In the case for 'next p' and 'next[0] p' there are ugly gaps in the operator symbols for suffix implication. This occurs in many places in the document. 2) In the case for 'next[m] p' m>0 there is an 'n' on the rhs. It should be an 'm'. 3) In the case for 's_eventually[m:$]p', why not use 'not always[m:$] not p' as the definition as in the case for 's_eventually[m:n]p'? s_next[m] s_eventually p = not next[m] not s_eventually p = not next[m] always not p = not always[m:$] not p 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). 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. BTW. I hope we have some mantis item for removing the restriction that clocks cannot be nested in the abstract syntax. 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" F.3.1.2 Rewrite rules for properties. ==================================== Similar comment to that of F.3.1.1 F.3.3 Satisfaction without local variables ========================================== Case for or: On the right hand side 'and' should be changed to 'or'. Case for accept_on: Should be changed to accord with Mantis 1757 where the definition is not in terms of 'least index'. (Same for F.3.6.1) Best Regards, Johan -- ------------------------------------------------------------ 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 ------------------------------------------------------------ -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Wed Dec 5 05:21:29 2007
This archive was generated by hypermail 2.1.8 : Wed Dec 05 2007 - 05:22:09 PST