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

Hi Doron,

In LTL.1932.20071030.pdf 16.12 in Syntax 16-14.

1) There is still an occurrence of the non terminal const_expression
that doesn't seem to occur in D4. (In the second case for next).

2) Why is the non terminal const_or_range_expression used in s_always
and eventually instead of cycle_delay_const_range_expression which is
used in always and s_eventually? Is the intention to allow s_always[n]
but not always[n] for example? I think only two number ranges should be
allowed in always, s_always, s_eventually and eventually. We already
have s_next[n] for expressing s_always[n] and next[n] for expressing
eventually[n].


Best Regards,

Johan M


On Mon, Oct 22, 2007 at 05:01:39PM +0200, Johan Mårtensson wrote:
> 
> 
> 
> 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
> ------------------------------------------------------------

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