SPECIFICATION Spec
CONSTANTS
    NumStages = 4
    MaxAttempts = 2
    ForceRerunOnRetry = TRUE
INVARIANTS
    TypeOK
    NeverTrustPartial
    NoConcurrentRuns
    CleanupAlways
PROPERTY
    MonotonicProgress
CHECK_DEADLOCK TRUE