[sv-ac] JH comments on 1932 Annex F changes

Hi Doron:

Below are my comments on the Annex F changes from 1932.

J.H.

1932 Review:  JH Notes 2008-01-07
---------------------------------

Changes to Annex F.

* Throughout.  Please align the fonts to the current usage in Annex F.  In the
  abstract grammars, non-terminals are in roman italic, while terminals are in
  courier or courier bold.  Keywords in the syntax (not comments) are in courier
  bold.

* p. 1, F.2.1, comment for accept_on.  Why is "accept_on" in angle brackets
  ("<>")?

* pp. 4-6, F.2.3.  1668 changed the notational conventions for Annex F.
  Lowercase r, s denote either clocked or unclocked sequences, and lowercase
  p, q denote either clocked or unclocked properties (all with possible 
  subscripts).  

  In some cases, I think that the lowercase should be used instead of 
  uppercase (which restricts either to clocked or unclocked).  E.g., in 
  F.2.3.2.2 I guess that lowercase p_1, p_2 can be used for "implies" and
  "iff". 

  It may be worth going back through all the derived operators to see 
  where we can relax to the notation for either clocked or unclocked entities.

* p. 6, F.2.3.2.8.  I think that there are some subtleties in defining

     (next p) \equiv (1 |=> p)

  that make this inequivalent to the PSL X.  I don't think it will be clear
  which rule for "|=>" should be used.

  Consider

     @(c) next strong(@(c) a)

  The definition says that this is equivalent to

     @(c) 1 |=> strong(@(c) a)

  Here I am not sure how to get rid of |=>.  Strictly speaking, strong(@(c) a)
  is clocked, so I should use

     @(c) 1 ##1 (@(1) 1) |-> strong(@(c) a)

  which is definitely not the same as PSL X.

  When I was thinking about 1296, I kept running into dissatisfaction with 
  the current definition of |=> in the clocked case, and I think we will need
  to make some decision in the future about what we want to do with |=>.

  Possibly, next should not be a derived operator at this time.  If you are
  happy with PSL X semantics for next, then I think it makes sense to write the
  semantics for next as a primitive operator like in PSL.

* p. 6, F.2.3.2.8.  I think that 

     s_eventually[m:$] p \equiv not(always[m:$] not p)

  should be a theorem.  Would this make a better definition?

* p. 6, F.2.3.2.8.  Why is m < n required in the definition of s_always[m:n] p?
  I think that this form needs to be defined for all m <= n.

* p. 8, F.3.1.1.  I thought the suggestion was to allow any sequence as first
  argument of T^s.  The notations introduced in 1668 say that capital R stands
  for an unclocked sequence and capital S stands for a clocked sequence.  I 
  recommend changing S (with and without subscripts) to r (with and without subscripts)
  in these rules, since r can stand for either a clocked or an unclocked sequence.

* p. 8, F.3.1.2.  Similar comment to the preceding.  I recommend changing Q to p
  (with and without subscripts) and S to r (with and without subscripts).

* p. 8, F.3.1.2.  I think that 

     T^p((@(c_2) P), c_1) = T^p(P,c_2)

  should be deleted.  It will be redundant with 

     T^p((@(c_2) p), c_1) = T^p(p,c_2)

  when Q is changed to p.

* p. 8, F.3.1.2.  If you make next a primitive as I have suggested above, then
  you will need to add a rewrite rule for it.

* p. 9, F.3.3.  The heading "F.3.3.1 Neutral satisfaction" appears within the
  text that is being changed, but this is not correct.  I think you should use
  this heading to identify where the text that is being changed is located.

* p. 9, F.3.3.  I recommend deleting the comma after "w^i |= b" in the second
  sub-bullet of the definition for accept_on.

* p. 10, F.3.3.3.  I don't think that the change is aligned with Draft 4.
  Draft 4 shows that the subscripts have already been deleted in a number of these 
  cases.  It is not correct to show the subscripts as still existing and to 
  specify their deletion as part of this proposal.

* p. 10, F.3.3.3.  I have been worried that we may not want to define non-vacuity 
  for derived operators by applying the primitive definitions to the semantic
  definition of the derived operator.  I think it is important to check these cases.

  If next is defined as primitive, then it needs a definition here.

* p. 10, F.3.3.3.  I'm not sure whether we can really get away with not defining
  non-vacuity for until.  We should discuss the technical issues.

* p. 11, F.3.6.1.  Change T^p(Q) to T^p(Q,1).












     


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