\* Online checkpointing specification
\* Default bounds: MaxSteps=10, NumCheckpoints=3

CONSTANTS
    MaxSteps = 10
    NumCheckpoints = 3

SPECIFICATION Spec

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

INVARIANT
    BufferBudget
    PinnedOrigin
    SpacingPowerOf2
    UniformSpacing
    BufferSorted
    CompletenessProperty

PROPERTY
    Termination
