Section H.3.1

LRM-151

Change (changes in red and blue):

EDITOR’S NOTE: The change request showed changing to. The original text already had. Should the be changed to, or is no change needed?

Section H.4.1

LRM-153

Change (restore |== to |=) (changes in red and blue):

·          w j,L0,L1 |= |== |=T(V).ended iff there exist 0 £ i £ j and L such that both w i, j, {}, L |== T(V) and L1 = L0 |D Θ L|V , where D = dom(L0) - (dom(L) Η V) .

 

EDITOR’S NOTE: I assumed that the |== symbol in the change request is the the same symbol as .

 

SVA 3.1A Draft 3 Errata, JH Group 2:  Errata in Appendix H

1. ERRATRUM JH3:  pp. 484-485, H.2.1.  There is a font inconsistency in the abstract grammars.  In the grammars for unclocked sequences, clocked sequences, and assertions, non-terminals are set in roman italic, while in the grammars for unclocked properties and clocked properties, non-terminals are set in courier italic.  The font for non-terminals should be roman italic.   For example, in the first line of the abstract grammar for unclocked properties, “P ::= R”  should be “P ::= R”.

 

2. ERRATRUM JH4:  pp. 484-485, H.2.1.  There is a spacing inconsistency in the abstract grammars.  In the grammars for unclocked sequences and clocked sequences, space is provided between tokens on the right-hand sides of productions, while in the grammars for unclocked properties and clocked properties such space is not provided.  One or the other sets of grammars should be changed.  This is an aesthetic issue. 

 

3. ERRATUM JH5:  p. 484, H.2.1, bottom of the page.  There seems to be space missing before the last sentence on the page.  Change

 

   ... non-degenerate unclocked sequence.See H.3.2 ...

 

to

 

   ... non-degenerate unclocked sequence.  See H.3.2 ...

 

4. ERRATUM JH6:  p. 485, H.2.1, the two sentences following the grammar for clocked properties.  There seems to be space missing between these two sentences.  Change

 

   ... non-degenerate clocked sequence.See H.3.2 ...

 

to

 

   ... non-degenerate clocked sequence.  See H.3.2 ...

 

5. ERRATUM JH7:  p. 485, H.2.2.  Delete the sentence

 

   The following auxiliary notions will be used in defining the semantics.

 

Rationale:  All references to these notions have been deleted.

 

6. ERRATUM JH8:  p. 485, H.2.2.  Delete the clause

 

   N, N1, N2 denote negation specifiers;

 

Rationale:  All references to negation specifiers have been deleted.

 

7. ERRATUM JH9:  p. 485, H.2.2.  Change

 

   P denotes an unclocked property

 

to

 

   P, P1, P2 denote unclocked properties.

 

Rationale:  H.2.3.5 refers to P1 and P2.

 

8. ERRATUM JH10:  p. 487, H.3.1.  Third bullet.  Change

 

   @(c) ( P )  |--->  @(c) P .

 

to

 

   @(c) ( P )  |--->  ( @(c) P ) .

 

Rationale:  The parentheses should not be lost.  I think they were in the change request.

 

9. ERRATUM JH11:  p. 487, H.3.1, last two bullets.  The fonts used for the clock rewrite rules for "and" and "or" do not match the style of the other bullets.  The terminals "@", "(", ")" should be set in courier "@", "(", ")" and the keywords "and", "or" should be set in courier bold "and", "or".

 

10. ERRATUM JH12:  H.3.2, p. 488.  The two dashed sub-bullet items under the the seventh bullet (first_match) need to be indented.

 

11. ERRATUM JH13:  p. 488, H.3.3.1.  In the first bullet under "Neutral satisfaction of assertions", change

 

   wi |= b

 

to

 

   \overline{w}i |= b

 

[The result should be like the overline in \overline{w}i |= c that precedes it.  I don’t know how to make word give me an overline.]

 

12. ERRATUM JH14:  p. 488, H.3.3.1.  In the third bullet under "Neutral satisfaction of assertions", delete “then”.  Also delete the parentheses around the clause after “iff”.

 

13. ERRATUM JH15:  pp. 488-489, H.3.3.1.  In the third bullet under "Neutral satisfaction of properties", change

 

   Ϊw

 

to

 

   Tw

 

(“T” is the sans-serif symbol that looks like "T".  You might be using an Arial "T" for it.)

 

14. ERRATUM JH16:  p. 489, H.3.3.1.  Change the remark at the end of this section from

 

   Remark:  It can be proved ...

 

to

 

   Remark:  Since w is non-empty, it can be proved ...

 

Rationale:  People have been confused about this because they forget that the assumption w non-empty applies throughout H.3.3.1.

 

15. ERRATUM JH17:  p. 489, H.3.3.2.  In the first bullet, change the italic "T" to "T".  This is the sans-serif symbol that looks like “T”.

 

16. ERRATUM JH18:  p. 489, H.3.3.2.  Change

 

   A tool checking for satisfaction of A by the finite word w should return

·         "true" if  w |= + A.

·         "false" if  w |/= - A.

·         "unknown" otherwise.

 

to

 

   A tool checking for satisfaction of A by the finite word w should return

·         "holds strongly" if  w |= + A.

·         "fails" if  w |/= - A.

·         "pending" or "holds weakly" otherwise.

 

Rationale:  This wording is to achieve alignment with PSL.

 

17. ERRATUM JH19:  p. 489, H.3.4, second  paragraph, second sentence.  Change

 

   sampled in the sequence

 

to

 

   sampled (i.e., assigned) in the sequence

 

Rationale:  Some people have (reasonably) expressed confusion that the local variable is being said to be "sampled" rather than "assigned".

 

18. ERRATUM JH20:  p. 491, H.3.5, first full sentence.  It is difficult to see visually the beginning of the definition of tight satisfaction because this sentence ends with displayed statements that are not centered.  I think the display formatting should be changed to paragraph formatting:  change

 

   It can be proved that this definition guarantees that

 

   w, L0, L1 |== R   implies   dom(L1) = flow(dom(L0), R) .

 

to

 

   It can be proved that this definition guarantees that w, L0, L1 |== R implies dom(L1) = flow(dom(L0), R) .

 

19. ERRATUM JH21:  p. 491, H.3.5, first bullet on the page.  Change the display formatting of

 

   L1 = {(v, e[L0, w0])} Θ L0|D

 

to paragraph formatting.

 

20. ERRATUM JH22:  p. 491, H.3.5, first bullet on the page.  Restore the definition

 

   and D = dom(L0) - {v}

 

that is struck out.

 

Rationale:  We need to keep this definition since we use "D" two lines above.

 

21. ERRATUM JH23:  p. 491, H.3.5, sixth bullet on the page.  The dashed sub-bullet items need to be indented.

 

22. ERRATUM JH24:  p. 491, H.3.5, eighth bullet on the page.  The dashed sub-bullet items need to be indented.

 

23. ERRATUM JH25:  p. 491, H.3.6.1, second paragraph.  Change

 

   rules defining neutral satisfaction of an assertion satisfaction are

 

to

 

   rules defining neutral satisfaction of an assertion are

 

24. ERRATUM JH26:  p. 492, H.4.1.  There are font errors in the second and fourth lines of this section.  In the second line, “V” should be italic “V”.  In the fourth line, “D” should be italic “D” (2 instances) and “V” should be italic “V” (2 instances).

 

25. ERRATUM JH27:  p. 493, H.5, second paragraph.  The keyword phrases “not” and “disable iff” appear in roman.  They should be changed to courier bold “not” and “disable iff”.

 

26. ERRATUM JH28:  p. 493, H.5, third paragraph, first sentence.  “depend” should be italic “depend”, as this word is being given a technical definition.

 

27. ERRATUM JH29:  p. 493, H.5, third paragrph.  Font errors:  “n” in “pn” should be italic as in “pn” (2 instances); “i” in “pi” should be italic as in “pi” (2 instances).

 

28. ERRATUM JH30:  p. 493, H.5, fourth paragraph, first sentence.  “dependency digraph” should be italic “dependency digraph”, as this phrase is being given a technical definition.

 

29. ERRATUM JH31:  p. 493, H.5, example in the middle of the fourth paragraph.  Courier “q” should be roman italic “q”; courier “r” should be roman italic “r” (2 instances).

 

30. ERRATUM JH32:  p. 493, H.5, fifth paragraph (the sentence defining “recursive”).  Courier “p” should be roman italic “p”.  “recursive” should be italic “recursive”, as this word is being given a technical definition.

 

31. ERRATUM JH33:  p. 493, H.5, last line.  Font error:  “L” should be italic “L”.