GryadkaCasRegister_variables.tla

\* msgs is the buffer of all messages. Messages can be delivered out of order or duplicated.
\* ops is the mapping from timestamp to CAS(old, new) for operations being proposed.
\* acceptorTS is the timestamp each acceptor is prepared for, only operations which match this value are accepted.
\* acceptorValTS is the timestamp of the last accepted value for each acceptor, or NoTS is none has been accepted yet.
\* acceptorValue is the last accepted value for each acceptor, or InitVal if none has been accepted yet.
\* history is the actual order of invoke/response actions for the operations identified by the timestamp.
VARIABLES msgs, ops, acceptorTS, acceptorValTS, acceptorValue, history