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 ofwantP
and the second gives the values ofwantQ
. -
Page 91, lines 18 and 19, and page 93, line 5.
csq
should beqcs
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 befull
. - 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 variableclock
. -
Page 177, line -4. Of course the initial task no longer includes
run
commands for theWatchdog
. - 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 aslisting-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
andS2
. 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 filecl-verif.pml
. The verification still works because only one snapshot is taken.
Last update on 24 August 2008.