Hi Ed, The language of that section in my change proposal is unclear. The first section in the change proposal Since for strong(sequence_expr) only one match is needed, properties of this form are evaluated to true if and only if the corresponding properties of the form strong(first_match(sequence_expr)) are evaluated to true respectively. As soon as a match of sequence_expr is determined, the evaluation of the property is considered to be true, and no other matches are required for that evaluation attempt. is meant to provide the reason why strong(sequence_expr) is equivalent to strong(first_match(sequence_expr)). This explanation will not do for the weak case since no match of the sequence is needed for truth of the weak embedding of the sequence. The second section in the change proposal should probably read something like the following to be in accordance with the semantic explanation for weak embedding found in the first paragraph of 16.12.1. It is also the case 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. Hence 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 problem with the original paragraph is that it provides the same reason for the equivalence in both the strong and weak cases, and I think this explanation is only valid in the strong case ("only one match is needed" is not really applicable in the weak case). Since only one match is needed, properties of the form sequence_expr, (weak(sequence_expr)), and (strong(sequence_expr)) are evaluated to true if and only if the properties first_match(sequence_expr), (weak(first_match(sequence_expr))) and (strong(first_match(sequence_expr))) are evaluated to true respectively. As soon as a match of sequence_expr is determined, the evaluation of the property is considered to be true, and no other Best Regards, Johan On Tue, Nov 20, 2007 at 05:27:03PM -0800, Eduard Cerny wrote: > Hello Johan, > > You wrote " It is also the case that a finite prefix of a trace > contradicts a sequence_expr if and only if it contradicts the > first_match of that sequence_expr." But what is the difference between > "contradicting the first_match or that sequence expression" and > contradicting any match of the sequence_expression"? Since there is no > first mathc there is no match at all. > > Thanks, ed > > > > -----Original Message----- From: owner-sv-ac@eda.org > > [mailto:owner-sv-ac@eda.org] On Behalf Of Johan Martensson Sent: > > Tuesday, November 20, 2007 11:20 AM To: sv-ac@eda.org; Bustan, Doron > > Subject: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata. > > > > Hi Doron, > > > > some problems I found in LTL.1932.20071114.pdf > > > > 16.12. (The paragraph beginning with: "The result of property > > evaluation is either true or false.") ====== > > > > There are lots of problems with this paragraph. > > > > 1) There are now boolean operators for implication and equivalence > > ('implies' and 'iff') which should perhaps be mentioned together > > with negation, disjunction and conjunction. 1) I think there should > > be dots, not hyphen between 'if' and 'else'. 2) There should be a > > comma between 'strong' and 'accept_on'. 3) 'and' between 'until' > > and 'eventually' should have different font from that of the > > operators. 4) 'implication' and 'followed_by' are not operators and > > should maybe have different font from that of the operators 'weak', > > 'strong' etc. 5) Maybe the strong variants of next, until, always > > and eventually, and the _with variants of until and s_until should > > also be listed. > > > > 1, 4 and 5 above point to a related set of problems with this > > paragraph: Should we list all the different operators here or should > > we use the grouping provieded by the various following subsections > > 16.12.2-16.12.16. It seems there is no uniform principle of > > reference chosen in this paragraph. > > > > Table 16.25 =========== > > > > The operators 'throughout', 'within', 'intersect', 'and' 'or', > > 'implies' and 'iff' are written with a initial capital letter. > > > > The operators 'implies' and 'iff' are rendered with different font > > from the others.. > > > > 16.12.1 Sequence property ========================= (The paragraph > > beginning with "Since only one match is needed, properties ...") > > > > This paragraph is a little strange. The discription seems to apply > > to strong embedding of sequences. For weak embedding not even one > > match of the sequence is required. > > > > If we decide to keep this section maybe it should be split in two > > giving different explanations for the weak and strong case > > respectively. > > > > REPLACE Since only one match is needed, properties of the form > > sequence_expr, (weak(sequence_expr)), and (strong(sequence_expr)) > > are evaluated to true if and only if the properties > > first_match(sequence_expr), (weak(first_match(sequence_expr))) and > > (strong(first_match(sequence_expr))) are evaluated to true > > respectively. As soon as a match of sequence_expr is determined, > > the evaluation of the property is considered to be true, and no > > other WITH > > Since for strong(sequence_expr) only one match is needed, > > properties of this form are evaluated to true if and only if the > > corresponding properties of the form > > (strong(first_match(sequence_expr))) are evaluated to true > > respectively. As soon as a match of sequence_expr is determined, > > the evaluation of the property is considered to be true, and no > > other matches are required for that evaluation attempt. > > > > It is also the case that a finite prefix of a trace contradicts a > > sequence_expr if and only if it contradicts the first_match of that > > sequence_expr. Hence 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. > > > > 16.12.1-16.12.16 ================ > > > > The headings of these sequences don't seem to be uniformly > > capitalized, for example 16.2.10 has initial capital in "Next > > property" but 16.2.11 has "always property". > > > > These headings seem to serve the purpose of naming different > > operator groups. For example an until property has one of the > > operators until, until_with, s_until or s_until_with as its top > > level operator. Maybe we should define explicit corresponding > > operator groups for use for examples in the section under 16.12 > > discussed above. > > > > This review was only partial, for this time :-(. > > > > Regards, > > > > Johan M > > > > On Wed, Nov 07, 2007 at 11:38:31AM +0100, Johan Martensson wrote: > > > Hi Doron, > > > > > > some further errors I found in LTL.1932.20071030.pdf > > > > > > 16.12. (The paragraph beginning with: The result of > > property evaluation > > > is either true or false.) > > > > > > REPLACE (dot after always, should be comma, no comman after > > followed by, > > > and between accept_on and reject_on should not be bold.) > > > > > > The result of property evaluation is either true or false. > > Properties > > > may be built from other properties or sequences using > > > instantiation, boolean operators (negation, disjunction, > > > conjunction, if...else, implication, followed_by weak, strong and > > > iff) and temporal > > operators > > > (next, always. until, eventually, accept_on and reject_on) > > described in > > > the following subclauses. > > > > > > WITH The result of property evaluation is either true or false. > > Properties > > > may be built from other properties or sequences using > > > instantiation, boolean operators (negation, disjunction, > > > conjunction, if...else, implication, followed_by, weak, strong and > > > iff) and > > temporal operators > > > (next, always, until, eventually, accept_on and reject_on) > > described in > > > the following subclauses. > > > > > > > > > > > > 16.12.9 followed_by property > > > > > > REPLACE (I don't think proceed is the right word here) The > > > followed_by construct specifies that the checking of a > > property is > > > required to proceed a match of a sequential antecedent WITH The > > > followed_by construct specifies that the checking of a > > property is > > > required to be preceded by a match of a sequential antecedent > > > > > > REPLACE (followed => followed_by, "at the end point of the match" > > > => "the end point of this match") Two forms of followed_by are > > > provided: overlapped using > > operator #-# and > > > nonoverlapped using operator #=#. For overlapped followed, > > there shall > > > be a match for the antecedent sequence_expr, where at the > > end point of > > > the match is the start point of the evaluation of the consequent > > > property_expr. For nonoverlapped followed_by, the start point of > > > the evaluation of the consequent property_expr is the clock > > tick after the > > > end point of the match. WITH Two forms of followed_by are > > > provided: overlapped using > > operator #-# and > > > nonoverlapped using operator #=#. For overlapped > > followed_by, there shall > > > be a match for the antecedent sequence_expr, where the end point > > > of this match is the start point of the evaluation of the > > > consequent property_expr. For nonoverlapped followed_by, the start > > > point of the evaluation of the consequent property_expr is the > > > clock > > tick after the > > > end point of the match. > > > > > > REPLACE (remove ##1 in two places) The followed_by operators are > > > the duals of the implication > > operators. > > > Therefore, sequence_expr #-# property_expr is equivalent to > > the following: > > > > > > not sequence_expr ##1 1 |-> not property_expr > > > > > > and sequence_expr #=# property_expr is equivalent to the > > > following: > > > > > > not sequence_expr ##1 1 |=> not property_expr WITH The followed_by > > > operators are the duals of the implication > > operators. > > > Therefore, sequence_expr #-# property_expr is equivalent to > > the following: > > > > > > not sequence_expr |-> not property_expr > > > > > > and sequence_expr #=# property_expr is equivalent to the > > > following: > > > > > > not sequence_expr |=> not property_expr > > > > > > 16.12.10 > > > > > > REPLACE (expression => const_expression, constants => > > const_expression, > > > constant_expression => const_expression) Weak next property > > > evaluates to true if property_expr holds > > at the next > > > clock tick or if there are no further clock ticks. To > > require the clock > > > tick to occur, use the strong form s_next property_expr. Weak next > > > property with expression evaluates to true if property_expr > > holds in the > > > specified of future clock ticks indicated by the constants, > > or if there > > > are not enough clock ticks for the property to complete the > > evaluation. > > > To require the necessary clock ticks to occur use the > > strong form s_next > > > [constant_expression] property_expr. WITH Weak next property > > > evaluates to true if property_expr holds > > at the next > > > clock tick or if there are no further clock ticks. To > > require the clock > > > tick to occur, use the strong form s_next property_expr. Weak next > > > property with const_expression evaluates to true if > > property_expr holds in the > > > specified of future clock ticks indicated by the > > const_expression, or if there > > > are not enough clock ticks for the property to complete the > > evaluation. > > > To require the necessary clock ticks to occur use the > > strong form s_next > > > [const_expression] property_expr. > > > > > > I just read to this poin this time. Hopefully I get some > > time to read > > > the rest. > > > > > > Best Regards, > > > > > > Johan > > > > > > > > > -- ------------------------------------------------------------ > > > Johan Mårtensson Office: +46 31 7451913 Jasper > > > Design Automation Mobile: +46 703749681 Arvid Hedvalls > > > backe 4 Fax: +46 31 7451939 411 33 Gothenburg, Sweden > > > Skype ID: johanmartensson > > > ------------------------------------------------------------ > > > > -- ------------------------------------------------------------ > > Johan Mårtensson Office: +46 31 7451913 Jasper > > Design Automation Mobile: +46 703749681 Arvid Hedvalls backe > > 4 Fax: +46 31 7451939 411 33 Gothenburg, Sweden > > Skype ID: johanmartensson > > ------------------------------------------------------------ > > > > > > -- 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 Arvid Hedvalls backe 4 Fax: +46 31 7451939 411 33 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 Nov 21 00:20:22 2007
This archive was generated by hypermail 2.1.8 : Wed Nov 21 2007 - 00:20:48 PST