Q on auxiliary vars again

14 views
Skip to first unread message

Alex Tim

unread,
Apr 13, 2020, 2:35:00 PM4/13/20
to tlaplus
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 satis fies 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 ) and EndRd(i) in SSpecL (LinearSnapshot )...Am not i right?

Thanks.

Alex Tim

unread,
Apr 14, 2020, 11:27:11 AM4/14/20
to tlaplus
Sorry, I understood the statement on p. 52. it's correct.

понедельник, 13 апреля 2020 г., 21:35:00 UTC+3 пользователь Alex Tim написал:
Reply all
Reply to author
Forward
0 new messages