Known errors in "Designing Reliable Distributed Systems" -------------------------------------------------------- * On page 117, Section 7.2.2, third line, there is a typo: |- Et = t' should of course be E |- t = t' * In Section 11.2.2, the "multicast" operator is declared to be a constructor, of sort Msg. Since a "multicast" message multicast mc from A to B ; C ; D gets reduced to a number of single messages (msg mc from A to B) (msg mc from A to C) (msg mc from A to D) then the multicast operator should NOT be a constructor, and its value sort should be "Configuration" instead of Msg. * On page 190, second line, "var" is missing just before "MC : MsgContent ." * On pages 265-266 I might allude to, but never state that "false" is the same as "not true" in Definition 16.2 and later. Maybe this was obvious, but maybe it should be said, at least to justify that we only really need the symbols true, p, not, and, until, and next. Otherwise, this fact might not be needed, because of the way Definition 16.6 is given. * This is NOT an error, since on page 264 (or elsewhere) I never say that we do not lose anything by assuming that all behaviors are infinite while doing LTL model checking. Most papers on temporal logics assume that behaviors are infinite. However, many (including the Manna-Pnueli books) allow both finite and infinite behaviors. Assuming that all behaviors are infinite allows us to define the semantics of the temporal operators without considering both cases. However, you DO lose something: you can no longer characterize that a behavior is finite (<> NOT (O True)) or that a behavior is infinite ([] (O True)). Quite often you can define an atomic proposition 'enabled' to mitigate this. So I just want to explicitly make clear that you lose something by making this simplifying assumption.