SPECIFICATION Spec

CONSTANTS
    Tabs   = {t1, t2}
    Budget = 3
    MaxGen = 3

INVARIANTS
    TypeOK
    SpendWithinBudget
    RotationSafety

PROPERTY
    NoZombieGrant

CHECK_DEADLOCK FALSE