SPECIFICATION Spec
CONSTANT GuardDist = TRUE
INVARIANT TypeOK
INVARIANT ServedIsOwnerAuthored
INVARIANT ServedCoherence
CHECK_DEADLOCK FALSE