My thanks to Robert Godfroid for raising the issues below (except as noted).

Errata

• Page 4, line 9. "if there is a some" should be "if there is some".
• Page 31, line 3. The last entry should be "Process P, n = 2".
• Page 44, line -4 and page 47 line 11. "Listing 3.8" should be "Listing 3.7".
• Page 54, line 17. "if and only there is" should be "if and only if there is".
• Page 54, footnote 4. "11. !wantP" should be "12. !wantP" (thanks to A. Burak Gurdag).
• Page 82. The editing of the jSpin output deleted an important line: Following the first assignment to wantP (the third statement executed), the first column gives the values of wantP and the second gives the values of wantQ.
• Page 91, lines 18 and 19, and page 93, line 5. csq should be qcs as specified in the #define in line 16.
• Page 99 line 8. "a language that not contain" should be "a language that does not contain".
• Page 109. In the diagram, (green, 20, false) should be (red, 20, false).
• Page 114, line 3. (line 20) should be (line 9).
• Page 117, line -14 and page 118, line 20 of Listing 7.6. nfull should be full.
• Page 128, lines -3,-4: "no errors have been be detected" should be "no errors have been detected".
• Page 166. Missing semicolon at the end of line 9 of Listing 11.3.
• Page 176, line -5. The value 2 is for the variable clock.
• Page 177, line -4. Of course the initial task no longer includes run commands for the Watchdog.
• Page 183, line 13: "is the same as at that" should be "is the same as that".
• Page 187, line 3: "a snapshot a set" should be "a snapshot is a set".

Software archive

• The programs for Chapter 7 have been renamed to correspond with the numbers of the Listings.
• The programs in the software archives have a GNU GPL copyright notice, so the line numbers will not correspond to those in the Listings in the text. For example, the line numbers in Listing 10.3 on page 160 do not correspond with those in the output shown on p. 161.
• Page 112. The modifications to Listing 7.4 must include changing the declaration of reply as {byte,byte}. This program has now been included in the software archive as listing-7-4-verify.pml.
• Page 114. The modified version of Listing 7.5 described in Section 7.2.2 is now included in the software archive as listing-7-5-run.pml.

Clarifications

• The first sentence on page 133 may give the wrong impression. Anytime a new input value (whether a string or a number) is entered in the VN software, Generate must be selected again.
• The algorithm for adding sparse matrices (Listing 11.4 on page 167) empties the channels S1 and S2. To preserve the data in those channels, use the technique shown in Listing 11.3, where the elements removed from the head of a channel are replaced on the tail of the channel.
• In Listing 11.22 on page 199, line 10 is not followed by recorded=true like line 15. This does appear in the source code in the file cl-verif.pml. The verification still works because only one snapshot is taken.

Last update on 24 August 2008.