SPECIFICATION Spec
\* All claims can expire, leaving a valid terminal state where no
\* action is enabled. This is the system quiescing, not a deadlock.
CHECK_DEADLOCK FALSE
CONSTANTS
    Identities = {id1, id2}
    Domains = {d1, d2}
INVARIANTS
    TypeOK
    NoPendingAndClaimed
    OneDomainOneOwner
    OneDomainOneClaim
    ClaimedByIdentity
    CfIdImpliesBound