SPECIFICATION PetersonSpec
INVARIANT PetersonTypeOK
INVARIANT PetersonIsMutex
PROPERTY PetersonIsFair