[sv-ac] partial review of 1932

Hi Folks:

It has been on my plate for a while to review 1932.

I have only begun reading the proposed changes to Annex F.
My comments so far are below.

I will continue.

J.H.


Review of proposed changes to Annex F
-------------------------------------

* F.2.1.  Abstract grammar for unclocked properties.  
  . Q --> P in the old text.
  . Parentheses are missing in the old and new text for binary operators 
    "or", "and", "|->".  These should be in courier.
  . For consistency, parentheses should be used in the new text for binary 
    operator <until>.  These should be in courier.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.


* F.2.1.  Abstract grammar for clocked properties.  
  . Parentheses are missing in the old and new text for binary operators 
    "or", "and", "|->".  These should be in courier.
  . For consistency, parentheses should be used in the new text for binary 
    operator <until>.  These should be in courier.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.
  . Why has the nested clock production been added?  If there is a compelling 
    reason to add this form for properties, then I expect it should be added
    for sequences as well.

* F.2.3.1.1.  Derived consecutive repetition operators
  . Ordinary courier should be used for terminal characters that are not in
    keyword operators.

* F.2.3.1.4.  Other derived operators.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.

* F.2.3.2.1.  Derived boolean operators.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.

* F.2.3.2.2.  Derived nonoverlapping implication operator.  
  . Ordinary courier should be used for terminal characters that are not in
    keyword operators.

* F.2.3.2.3.  Derived conditional operators.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.

* F.2.3.2.4.  Derived followed_by operators.
  . folowed_by --> followed_by.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.
  . These rules could be unified by using the notations that do not care about
    clocks, lowercase r or s for sequence, lowercase p or q for property.
    See the proposed changes to F.2.2 in 1668.  

* F.2.3.2.5.  Derived reset operator.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.
  . There is a parenthesis mismatch on the RHS.
  . Decide whether parentheses are needed for using reject_on in the Annex and
    be consistent between the grammar and these rules.
  . Why is there no rule for clocked property?  I guess that the rules for clocked
    and unclocked should be unified using the notation that does not care about
    clocks (see above).

* F.2.3.2.6.  Derived unbounded temporal operators.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.
  . Why are there no rules for clocked properties?  I guess that the rules for clocked
    and unclocked should be unified using the notation that does not care about
    clocks (see above).
  . P --> P_1 in the rule for weak until.  I prefer referring to the derive always
    here rather than copying out the RHS of the derived always.
  . Parentheses are not written consistently in the "until with" form.
  . Why aren't the strong and weak "until with" forms parallel?  Is there a technical
    reason to write these differently?

* F.2.3.2.7.  Derived bounded temporal operators.
  . Bold courier should be used for the keyword operators.  Ordinary courier
    should be used for other terminal characters.
  . Why are there no rules for clocked properties?  I guess that the rules for clocked
    and unclocked should be unified using the notation that does not care about
    clocks (see above).
  . Why aren't <next[0]>/next[0] the strong/weak clock alignment operators rather than
    no-ops?  I don't like the idea of wasting this syntax on no-ops.
  . I think that it should be possible to reduce the number of derived rules by
    defining the parameterized weak next in terms of the parameterized strong next.


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