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

Hi,

I have the following additional comment on  LTL.1932.20071005.pdf.



p.5

 Properties may be built from other properties or sequences using
 instantiation, boolean operators (negation, disjunction, conjunction,
 if...else, implication and iff) and temporal operators (next, always.
 until, until_with, eventually, accept_on and reject_on) described in the
 following subclauses.                                                                  
 
I think the operators 'weak', 'strong' and the strong versions s_next,
s_always.  s_until, s_until_with and s_eventually should also be
mentioned here.


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
> ------------------------------------------------------------
> 
> -- 
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 

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