\* Hint-based checkpoint allocation specification
\* Default bounds: NumSteps=6, NumCheckpoints=3

CONSTANTS
    NumSteps = 6
    NumCheckpoints = 3

SPECIFICATION Spec

\* Termination is expected — the "done" state has no successor.
CHECK_DEADLOCK FALSE

INVARIANT
    RequiredIncluded
    BudgetRespected
    AllocationExact
    AllInRange

PROPERTY
    Termination
