-------------------------- MODULE MutualExclusion ---------------------------
CONSTANT Thread
VARIABLE tstate

METypeOK == tstate \in [Thread -> {"noncs", "waiting", "cs", "exiting"}]

MEMutexInvariant == 
  \A t1, t2 \in Thread : (tstate[t1] = "cs") /\ (tstate[t2] = "cs") => (t1=t2)

MEInit == tstate = [t \in Thread |-> "noncs"]
-----------------------------------------------------------------------------
METry(t) == /\ tstate[t] = "noncs"
            /\ tstate' = [tstate EXCEPT ![t] = "waiting"]

MEEnterCS(t) == /\ tstate[t] = "waiting"
                /\ \A tt \in Thread : tstate[tt] # "cs"
                /\ tstate' = [tstate EXCEPT ![t] = "cs"]

MEExitCS(t) == /\ tstate[t] = "cs"
               /\ tstate' = [tstate EXCEPT ![t] = "exiting"]

MEFinish(t) == /\ tstate[t] = "exiting"
               /\ tstate' = [tstate EXCEPT ![t] = "noncs"]

MENext == \E t \in Thread : 
            METry(t) \/ MEEnterCS(t) \/ MEExitCS(t) \/ MEFinish(t)
-----------------------------------------------------------------------------
MEDeadlockFree  == 
  MEInit /\ [][MENext]_tstate /\ (\A t \in Thread : WF_tstate(MEFinish(t)))
    /\ WF_tstate(\E t \in Thread : MEEnterCS(t))
MEStarvationFree == 
  MEInit /\ [][MENext]_tstate /\ (\A t \in Thread : WF_tstate(MEFinish(t)))
    /\ (\A t \in Thread : SF_tstate(MEEnterCS(t)))
=============================================================================