CONSTANT Thread = {t1}
         NotAThread = NotAThread
SPECIFICATION S_MEStarvationFree
PROPERTY TheSpec \* MCSSpec