SPECIFICATION Spec
INVARIANT Safety
CHECK_DEADLOCK FALSE
CONSTANTS
    MaxHolds = 2