SPECIFICATION Spec
CONSTANTS
  Missions = {m1, m2}
  Atts = {a1, a2}
  Reqs = {r1, r2}
  NoMission = NoMission
  MaxBudget = 3
  Costs = {1, 2}
INVARIANT TypeOK
INVARIANT BudgetIsHardCap
INVARIANT SpendRequiresFunding
INVARIANT MissionsComeFromAttestations
PROPERTY BudgetBindsOnce
PROPERTY NoNewSpendAfterRevoke
CHECK_DEADLOCK FALSE