RE: [sv-ac] Re: 1932 LTL.1932.20071114.pdf some errata.

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.
> 
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.