SPECIFICATION QueueSpec
CONSTANTS
Mode = "Unordered"
GoalBound = 1
EditBound = 2
StampBound = 0
TurnBound = 1
FailBound = 1
INVARIANTS TypeOK AutoProvenance SuccessReset FailureEvidence NoEarlyResume UsageEvidence StopCancels HumanStops
PROPERTIES QueueProgress
CHECK_DEADLOCK FALSE