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

[tlaplus] Q on auxiliary vars again

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?


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.