SPECIFICATION Spec
\* Quiescence is legal: ids are modeled as never reused, so a state where
\* every id has been minted and removed has no enabled action. That is the
\* finite id pool running dry, not a stuck protocol.
CHECK_DEADLOCK FALSE
CONSTANTS
    Ids = {s1, s2, s3}
INVARIANTS
    TypeOK
    Disjoint
    OwnedNeverSwept