\* Revolve base checkpointing specification
\* Default bounds: NumSteps=8, NumCheckpoints=3

CONSTANTS
    NumSteps = 8
    NumCheckpoints = 3

SPECIFICATION Spec

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

INVARIANT
    BudgetInvariant
    PositionRangeInvariant
    SortedCheckpoints
    InitialStateStored
    WorkStackBoundsInvariant
    CompletenessProperty

PROPERTY
    Termination
