SPECIFICATION Spec
CONSTANTS
    InitMem = 1
    ResetThreshold = 3
    EngineBudget = 6
    IsolateLimit = 12
    MaxGrow = 2
    MaxRequests = 4
INVARIANTS
    TypeOK
    FreshStart
    BelowKill
    BoundedOvershoot
PROPERTY GrowOrReset
CHECK_DEADLOCK FALSE