SPECIFICATION PartSpec
CONSTANTS
    First = "paused"
    Last = "active"
    Mode = "Reconcile"
    GoalBound = 1
    EditBound = 2
    StampBound = 0
    TurnBound = 1
    FailBound = 1
INVARIANTS TypeOK FreshRepair AutoProvenance SuccessReset FailureEvidence NoEarlyResume UsageEvidence StopCancels HumanStops
PROPERTIES RecoveryProgress StopProgress HoldProgress
CHECK_DEADLOCK FALSE