SPECIFICATION FairSpec
INVARIANT TypeOK
INVARIANT MutualExclusion
PROPERTY StarvationFreedom