SPECIFICATION Spec
CONSTANT UseLock = TRUE
INVARIANT TypeOK
INVARIANT GrantSurvives
CHECK_DEADLOCK FALSE