SPECIFICATION Spec
\* Quiescence is legal: every mission and pending record can reach a terminal
\* state (closed / gone), after which no action is enabled for it; with the
\* finite id pools fully terminal, the system rests. Java TLC needs the
\* equivalent -deadlock flag without this line.
CHECK_DEADLOCK FALSE
\* Id pools are singletons/pairs: every checked property is per-record, so
\* record count only adds interleaving. Users and Resources stay at 2 — they
\* are what exercise ApproverBinding and AttenuationNeverWidens. The larger
\* MissionIds = {m1, m2} model (2.8M distinct states) passes Java TLC in 12s.
CONSTANTS
    Users = {u1, u2}
    MissionIds = {m1}
    PendingIds = {p1, p2}
    Resources = {r1, r2}
    MaxAmt = 1
    NoUser = NoUser
INVARIANTS
    TypeOK
    CodeSingleUse
    ApproverBinding
    AttenuationNeverWidens
    NoIssuanceAfterClose
    OneShotPickup
PROPERTIES
    ClosedIsTerminal
    GoneIsTerminal