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.