GryadkaCasRegister_initial_state.tla

Messages == [type: {"prepare"}, acceptor: Acceptors, ts: Timestamps]
     \union [type: {"promise"}, acceptor: Acceptors, ts: Timestamps,
             prevTS: Timestamps \union {NoTS}, prevVal: Values]
     \union [type: {"accept"}, acceptor: Acceptors, ts: Timestamps, val: Values]
     \union [type: {"accepted"}, acceptor: Acceptors, ts: Timestamps, val: Values]
\* Each operation represents a CAS from an oldVal to a newVal. In Gryadka,
\*     reads are treated the same as CAS(val, val)
Operations == [oldVal: Values, newVal: Values]
Events == [type: {"invoke", "response"}, ts: Timestamps]

TypeOK == /\ msgs \subseteq Messages
          /\ ops \in [Timestamps -> Operations]
          /\ acceptorTS \in [Acceptors -> Timestamps \union {NoTS}]
          /\ acceptorValTS \in [Acceptors -> Timestamps \union {NoTS}]
          /\ acceptorValue \in [Acceptors -> Values]
          /\ history \in Seq(Events)

Init == /\ msgs = {}
        /\ ops \in [Timestamps -> Operations]
        /\ acceptorTS = [a \in Acceptors |-> NoTS]
        /\ acceptorValTS = [a \in Acceptors |-> NoTS]
        /\ acceptorValue = [a \in Acceptors |-> InitVal]
        /\ history = <<>>