[sv-ac] review of mantis 1381

After seeing Ed's remark on 1381, I was prompted 
to have a closer look.  Below is what I found.

J.H.


Editorial Problems:
-------------------

1. Draft 1, p. 304, 17.13.6, first sentence:  Editor has 

     An evaluation of a property is either vacuous or non-vacuous.

   while mantis 1381 has

     An evaluation attempt of a property is either vacuous or non-vacuous.


2. Draft 1, p. 304, 17.13.6, second sentence:  Editor has 

     for seven kinds of properties

   while mantis 1381 has
 
     for the seven kinds of properties

   I think the definite article should be used because in 17.11, p. 263,
   the LRM says

     There are seven kinds of propety:  sequence, negation, disjunction,
     conjunction, if..else, implication, and instantiation.

   The mantis proposal should probably have said "for the seven kinds 
   of property".

   In the future, as more property kinds are added, e.g. due to addition
   of LTL operators, it may be a good idea to stop counting them.  

3. Draft 1, p. 304, 17.13.6, item b).  Font mismatch between italic roman
   "property_expr" and italic courier "property_expr".  Italic roman 
   seems to be used more often throughout these items.

4. Draft 1, p. 304, 17.13.6, item c).  Editor has

     or the underlying evaluation of property_expr2 is non-vacuous

   while mantis 1381 has

     or the underlying evaluation attempt of property_expr2 is non-vacuous


5. Draft 1, p. 304, 17.13.6, item d).  Editor has

     or the underlying evaluation of property_expr2 is non-vacuous

   while mantis 1381 has

     or the underlying evaluation attempt of property_expr2 is non-vacuous

6. Draft 1, p. 304, 17.13.6, item e).  Font mismatch between italic courier
   "expression_or_dist" and italic roman "expression_or_dist".  Should
   be italic roman to match the other items.

7. Draft 1, p. 304, 17.13.6, item f).  Editor has

     that starts at end point of the match

   while mantis 1381 has

     that starts at the end point of the match

8. Draft 1, p. 305, 17.13.6.  Editor has

     An evaluation of a property of the form disable iff

   while mantis 1381 has

     An evaluation attempt of a property of the form disable iff


Other Problems:
---------------

a. Draft 1, 17.13.5, p. 289.  I agree with Ed that we seem to have 
   lost something with the sentence that is struck out.  However, 
   I think that we never actually solved the problem here.  We need
   to decide what happens if the enabling condition is false:

   1. is there no evaluation attempt at all?
   2. or is there a vacuous evaluation attempt?

   The second is bad for a "cover property", since then we seem
   to be forced to say that there is a vacuous attempt that we 
   do not want to call a hit.  I think that Ed's suggested language 
   is aligned with the first.

b. Draft 1, E.3.3.3, p. 571.  "Let ..., then ... ." is not a proper
   sentence structure.  It should be split into two sentences,
   "Let ... .  Then ... .".

c. Draft 1, E.3.3.3., p. 571.  There should not be a comma in 
  "iff there exists i >= 0, such that".

d. Draft 1, E.3.3.3, p. 572.  "\cdot" is not used elsewhere for word
   concatenation.

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