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