SPECIFICATION Spec

CONSTANTS
    Clients = {c1, c2}
    Keys = {k1, k2}
    MaxClock = 3
    MaxWrites = 3
    NoRec = NoRec

INVARIANT TypeOK
INVARIANT Convergence
INVARIANT ServerStoreIsLogMax
INVARIANT LogSeqDense
INVARIANT CursorInRange

PROPERTY Safety

CHECK_DEADLOCK FALSE