SPECIFICATION Spec
CONSTANTS
  Codes = {c1, c2}
  Grants = {g1, g2}
  NoGrant = NoGrant
  MaxBudget = 3
  Costs = {1, 2}
  MaxRefresh = 2
INVARIANT TypeOK
INVARIANT BudgetIsHardCap
INVARIANT CodeMintsAtMostOneGrant
INVARIANT GrantsComeFromCodes
PROPERTY NoSpendAfterRevoke
CHECK_DEADLOCK FALSE