GryadkaCasRegister_constants.tla

\* Timestamps is the set of possible timestamps for operations to choose from.
\*     Each operation uses a unique timestamp.
\* Values is the set of possible values to set the register to.
\* Acceptors is the set of nodes which act as acceptors in the paxos sense.
\* Quorums is the set of all possible quorums, typically simple majorities.
CONSTANTS Timestamps, Values, Acceptors, Quorums

ASSUME Timestamps \subseteq Nat
ASSUME IsFiniteSet(Timestamps)
NoTS == -1
ASSUME NoTS \notin Timestamps

ASSUME Quorums \subseteq SUBSET Acceptors
ASSUME \A q1, q2 \in Quorums : q1 \intersect q2 /= {}

\* The initial value is chosen arbitrarily
InitVal == CHOOSE v \in Values : TRUE