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

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

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