SPECIFICATION Spec
CONSTANTS
    MaxV = 2
    Readers = {r1, r2}
INVARIANTS
    TypeOK
    NoDanglingIndex
    MetaNeverAheadOfArtifact
    ReaderSafety