Skip to content

Instantly share code, notes, and snippets.

@grogers0

grogers0/GryadkaCasRegister_constants.tla

Created May 31, 2017 22:19
Download ZIP

Revisions

  1. grogers0 created this gist May 31, 2017.
    17 changes: 17 additions & 0 deletions GryadkaCasRegister_constants.tla
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,17 @@
    \* 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