Hi Akash,
The term “dense set” should appear only in the appendix, and its definition is given there.
If the definition does not give you an intuitive idea of what it means, thinking about the example of the set of ordered pairs of finite-digit numbers should help.
If there any things in the book that you did not learn in your classes and are not defined
in the book, please let me know.
Cheers,
Lelie Lamport
From:
tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of
Akash
Sent: Tuesday, January 30, 2024 11:11
To: tlaplus@xxxxxxxxxxxxxxxx
Subject: Re: [tlaplus] Re: Draft of New TLA Book
Hi Leslie,
I'm super interested in understanding TLA, but I don't understand the terms you use, like dense set, for example.
Which branches of math knowledge are you referring to? And prerequisite for knowing these terms. As a CS student, I've only studied Discrete
Mathematics and Calculus.
Hi Lorin,
Thanks for finding all these errors. One thing you reported is not an error:
p297 A subset S of a metric space M is said to be dense iff C(S) = [M].
-> should be [S]?
This is the correct definition of a dense set. C(S) = S is the definition
of a closed set.
Cheers,
Leslie
Hi Leslie:
Thanks for the response. I also found what appear to be a few minor errors/typos. These are from version of 2 January
2024. Errors are indicated by [square brackets]:
p158, 5.1.2. Let an S-State be a state of AddS, which is an assignment of values to the variables u,v, w and [end] of
AddS;
p162 all other steps must refine stuttering steps of [AddSeq]
p175 In particular, sem_LM equals 0 iff pc_LM(p) equals [pc] or exit for ...
p179 Figure 5.3, last row, last column: pc_OB(p) = [cs]
p179 By [(4.15)], we can do this by proving:
p212 We then replace DispOrNot in [ICen2] by ...
p237 If our strategy has been successful thus far and qBar = [pq] at the beginning of the step, then a BeginPOEnqpq step
implies qBar′ = [pq]′.
p237 Let's call a state in which there is a datum in elts that is not in beingAdded [] a blocked state.
p239 3. Following each BeginPOEnq pq step such that Len (pg ′ ) > Len (pg ) (which implies [eq] = ⟨⟩), s adds Len(pg′)
− Len(pg) stuttering steps.
p296 For a metric space M , the distance \^{δ}(p, [M]) from p
∈ M ...
p297 For any metric space M and S
⊆ M , any element p of M with [d](p,S) = 0 ...
p297 A subset S of a metric space M is said to be dense iff C(S) = [M].
On Wednesday, January 17, 2024 at 4:33:25 PM
UTC-8 Leslie Lamport wrote:
Hi Lorin,
Thank you for finding a serious error in the book. The inductive invariant Inv in the book is
strong enough to prove mutual exclusion, but not deadlock freedom. That invariant allows process 1 to halt in its noncritical section with x[1] = TRUE, which will not allow process 0 to enter its critical section. A stronger inductive invariant is needed
to prove liveness. This will be corrected in the next released version. Meanwhile, I suggest that you find the necessary inductive invariant yourself.
I’m embarrassed that I didn’t notice such an error. I think it happened because the TLA+ version
that I model checked had the correct invariant. When I checked my proof, I must have been thinking Inv was the invariant in the TLA+ version. I believe a significant amount of time passed between when I wrote Section 4.2.5.2 that contains the invariant and
the current version of Section 4.2.5.3 containing the liveness proof. That’s probably why I didn’t notice that the TLA+ version of the invariant was not the one in the book.
Cheers,
Leslie
I have a question about section
4.2.5.3: Proving Liveness
On page 134, the proof sketches for edge 5 and edge 7 read:
> edge 5 This is an implication since ☐Inv implies that if process 1 is forever at ncs, then x (1) is forever false.
> edge 7 This is an implication, because Inv and pc(1) = w4 imply ¬x (1).
> We define Inv to equal (4.6), with TypeOK defined by (4.17).
According to (4.6) on p122, this would mean:
/\ \A p \in {0,1): /\ (pc(p) \in {w2, cs}) => x(p))
/\ (pc(p) = cs) => (pc(1-p)\= cs)
Given the above definition for Inv, I can't see how ☐Inv could be used to imply ☐¬x(1), given that the only place that
x(p) appears in Inv (other than TypeOK) is in the consequent of an implication. What am I missing here? (Am I using the wrong Inv?)
On Wednesday, January 3, 2024 at 11:14:24 AM
UTC-8 Leslie Lamport wrote:
A draft of a new book I have tentatively titled
A Science of Concurrent Programs is available
here. The book explains the scientific principles underlying the TLA+ language. It contains a lot of math. All the math beyond high school algebra is explained, but it will be
tough going for readers who haven't taken an introductory university math class for computer science students that covers things like sets and logic. The book contains little discussion of how TLA+ is used in practice, but it explains why TLA+ is what it
is.
This is a preliminary version and I welcome comments, suggestions, and questions. Anyone
who is the first to report any error will be thanked in the final version.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/4471dd6a-08d2-4aea-8f8f-140a81a401f4n%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/LV2PR21MB322921E13D5EAF3419284511B87E2%40LV2PR21MB3229.namprd21.prod.outlook.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/CAFZmCwCWFUFQW10xb%2B9HmWvqmmfSNFtrVbmP2oT_EnENPPUH%3DQ%40mail.gmail.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/LV2PR21MB3229CD7EE994B8C259A20DB5B87D2%40LV2PR21MB3229.namprd21.prod.outlook.com.
|