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

*From*: Alex Tim <alex.timimin@xxxxxxxxx>*Date*: Tue, 14 Apr 2020 08:27:11 -0700 (PDT)*References*: <f7fa34ba-76b0-4a17-8b03-bf3fe5107c38@googlegroups.com>

Sorry, I understood the statement on p. 52. it's correct.

понедельник, 13 апреля 2020 г., 21:35:00 UTC+3 пользователь Alex Tim написал:

-- понедельник, 13 апреля 2020 г., 21:35:00 UTC+3 пользователь Alex Tim написал:

Hello allThe question is on TLA + axiliary variables againon the p. 52 it is stated thatThus, 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 ) actionfor a reader i .Is it correct? or it meant the weak fairness requirement of the EndOp(i)?On p. 55"...Letbe the formula obtained from a formula F of module LinearSnapshot by replacing mem withFand istate withmem..."istatethen "..The behavior satisfies, so this sequence of actions must start with aSSpecLstep, contain aBeginRd(i )step, and end with anDoRd(i )step." But there are no formulas BeginRd(i )EndRd(i ),

DoRd(i )and EndRd(i) in SSpecL (LinearSnapshot )...Am not i right?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/e16f6d63-9e63-4e78-953e-84eabfdc5682%40googlegroups.com.

**References**:**[tlaplus] Q on auxiliary vars again***From:*Alex Tim

- Prev by Date:
**[tlaplus] Q on auxiliary vars again** - Next by Date:
**[tlaplus] [Q on multiple agent update in step]** - Previous by thread:
**[tlaplus] Q on auxiliary vars again** - Next by thread:
**[tlaplus] [Q on multiple agent update in step]** - Index(es):