[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "'Leslie Lamport' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Mon, 29 Jan 2024 20:21:08 +0000*Accept-language*: en-US*Msip_labels*: MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ActionId=fdcb4ff0-c1e8-4810-9fbd-5b178c14341f;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_ContentBits=0;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Enabled=true;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Method=Standard;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_Name=Internal;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SetDate=2024-01-29T20:18:24Z;MSIP_Label_f42aa342-8706-4288-bd11-ebb85995028c_SiteId=72f988bf-86f1-41af-91ab-2d7cd011db47;*References*: <AQHaR3CM19eYLw8NOUicOkT3F9jut7DetQdg> <38ecd338-90a9-4fbf-827d-4d6a04d2bcfbn@googlegroups.com> <bef439e7-6a6c-4058-8366-a544088b5666n@googlegroups.com> <LV2PR21MB32298E6ADFD46A3328D6F0F8B8712@LV2PR21MB3229.namprd21.prod.outlook.com> <4471dd6a-08d2-4aea-8f8f-140a81a401f4n@googlegroups.com>*Thread-index*: AQHaR3CM19eYLw8NOUicOkT3F9jut7DetQdggBGqZACAAPJT4A==*Thread-topic*: [tlaplus] Re: Draft of New TLA Book

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; -> should be [fin]? p162 all other steps must refine stuttering steps of [AddSeq] -> should be [Add]? p175 In particular, sem_LM equals 0 iff pc_LM(p) equals [pc] or exit for ... -> should be [cs]? p179 Figure 5.3, last row, last column: pc_OB(p) = [cs] -> should be [exit]? p179 By [(4.15)], we can do this by proving: -> should be [(4.12)]? p212 We then replace DispOrNot in [ICen2] by ... -> should be ICen1? 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]′. -> should be [pg]? p237 Let's call a state in which there is a datum in elts that is not in beingAdded [] a blocked state. -> missing [or in pg]? p239 3. Following each BeginPOEnq pq step such that Len (pg ′ ) > Len (pg ) (which implies [eq] = ⟨⟩), s adds Len(pg′) − Len(pg) stuttering
steps. -> should be [eb]? p296 For a metric space M , the distance \^{δ}(p, [M]) from p
∈ M ... -> should be [S]? p297 For any metric space M and S
⊆ M , any element p of
M with [d](p,S) = 0 ... -> should be [\^{δ}]? p297 A subset S of a metric space M is said to be dense iff C(S) = [M]. -> should be [S]? Take care, Lorin On Wednesday, January 17, 2024 at 4:33:25 PM
UTC-8 Leslie Lamport wrote:
--
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. |

**Follow-Ups**:**Re: [tlaplus] Re: Draft of New TLA Book***From:*Akash

**References**:**[tlaplus] Draft of New TLA Book***From:*Leslie Lamport

**[tlaplus] Re: Draft of New TLA Book***From:*Lorin Hochstein

**RE: [tlaplus] Re: Draft of New TLA Book***From:*'Leslie Lamport' via tlaplus

**Re: [tlaplus] Re: Draft of New TLA Book***From:*Lorin Hochstein

- Prev by Date:
**Re: [tlaplus] Re: Draft of New TLA Book** - Next by Date:
**[tlaplus] Action A can only be followed by Action B** - Previous by thread:
**Re: [tlaplus] Re: Draft of New TLA Book** - Next by thread:
**Re: [tlaplus] Re: Draft of New TLA Book** - Index(es):