GryadkaCasRegister_invariants.tla

FiniteSeq(S) == UNION {[1..n -> S] : n \in 1..Cardinality(S)}
SeqAsSet(S) == {S[i] : i \in DOMAIN S}

HistoryIsLinearizable == \E order \in {<<>>} \union FiniteSeq(Timestamps) :
    /\ \A H \in SeqAsSet(history) : H.type = "response" => H.ts \in SeqAsSet(order)
    /\ \A H1_i, H2_i \in DOMAIN history :
        (history[H1_i].type = "response" /\ history[H2_i].type = "invoke" /\ H1_i < H2_i) =>
            (
                history[H2_i].ts \in SeqAsSet(order) =>
                    \E i1, i2 \in DOMAIN order :
                        /\ order[i1] = history[H1_i].ts
                        /\ order[i2] = history[H2_i].ts
                        /\ i1 < i2
            )
    /\ \A i1, i2 \in DOMAIN order :
        i2 = i1 + 1 => ops[order[i1]].newVal = ops[order[i2]].oldVal
    /\ order /= <<>> => InitVal = ops[order[1]].oldVal

Inv == /\ TypeOK
       /\ HistoryIsLinearizable