SPECIFICATION Spec
\* Quiescence is legal: with the finite challenge pool, a state where every
\* (tenant, challenge) pair has been consumed has no enabled action. That is
\* the never-repeats encoding running dry, not a stuck protocol.
CHECK_DEADLOCK FALSE
CONSTANTS
    Tenants = {t1, t2}
    Challenges = {c1, c2}
INVARIANTS
    TypeOK
    NoReplay