SPECIFICATION Spec
CONSTANTS
Mode = "Local"
GoalBound = 1
EditBound = 1
StampBound = 1
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset FailureEvidence NoEarlyResume UsageEvidence
PROPERTIES RecoveryProgress
CHECK_DEADLOCK FALSE