[sv-ac] 1932 LTL.1932.20071005.pdf partial review.

LTL.1932.20071005.pdf partial review 2007-10-22
===============================================

p.2-3) Non terminals const_expression and range_expression don't seem to
occur in D4. I guess constant_expression and
cycle_delay_const_range_expression can be used instead.

Also I think for symmetry between always and eventually, the parameter
to those operators should be a cycle_delay_const_range_expression and to
next a constant_expression. I.e. for example 'eventually [3] P' should
not be allowed.

REPLACE
| next property_expr 
| next [const_expression] property_expr 
| s_next property_expr
| s_next [const_expression] property_expr 
| always property_expr 
| always [range_expression] property_expr 
| s_always [range_expression] property_expr 
| s_eventually property_expr 
| eventually [const_or_range_expression] property_expr 
| s_eventually [const_or_range_expression] property_expr

WITH
| next property_expr 
| next [constant_expression] property_expr 
| s_next property_expr
| s_next [constant_expression] property_expr 
| always property_expr 
| always [cycle_delay_const_range_expression] property_expr 
| s_always [cycle_delay_const_range_expression] property_expr 
| s_eventually property_expr 
| eventually [cycle_delay_const_range_expression] property_expr 
| s_eventually [cycle_delay_const_range_expression] property_expr

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