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

*From*: Alex Tim <alex.timimin@xxxxxxxxx>*Date*: Mon, 13 Apr 2020 11:35:00 -0700 (PDT)

Hello all

The question is on TLA + axiliary variables again

on the p. 52 it is stated that

Thus, a read need never terminate, so the algorithm does not satisfy the liveness requirement of a snapshot algorithm namely, it does not satisfy the weak fairness requirement of the DoOp(i ) action

for a reader i .

Is it correct? or it meant the weak fairness requirement of the EndOp(i)?

On p. 55

"...Let **F** be the formula obtained from a formula F of module LinearSnapshot by replacing mem with **mem **and istate with **istate**..."

then "..The behavior satisfies **SSpecL**, so this sequence of actions must start with a __BeginRd__(i ) step, contain a __DoRd__(i ) step, and end with an __EndRd__(i ) step." But there are no formulas BeginRd(i )**,**

DoRd(i )

Thanks.

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/f7fa34ba-76b0-4a17-8b03-bf3fe5107c38%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Q on auxiliary vars again***From:*Alex Tim

- Prev by Date:
**Re: [tlaplus] Can't find the paxos.tla as shown in the Leslie's tutorial lecture 7 on youtube.** - Next by Date:
**[tlaplus] Re: Q on auxiliary vars again** - Previous by thread:
**Re: [tlaplus] Can't find the paxos.tla as shown in the Leslie's tutorial lecture 7 on youtube.** - Next by thread:
**[tlaplus] Re: Q on auxiliary vars again** - Index(es):