------------------------- MODULE MutexImplementation ------------------------ 
EXTENDS MutualExclusion, Naturals, Sequences

VARIABLE stuttering, iFace, pendingQ

NotAThread == CHOOSE n : n \notin Thread

s_vars == <<tstate, stuttering, pendingQ, iFace>>

initT == CHOOSE t \in Thread : TRUE

S_MEInit == /\ MEInit 
            /\ stuttering = [t \in Thread |-> 0]
            /\ iFace = [arg |-> <<initT, "exit">>, aBit |-> 0, 
                        rtn |-> <<initT, "OK">>,   rBit |-> 0]
            /\ pendingQ = << >>
-----------------------------------------------------------------------------
Remove(i, q) == [k \in 1..(Len(q)-1) |-> IF k < i THEN q[k] ELSE q[k+1]]
RemoveFromPendingQ(t) ==
    Remove(CHOOSE i \in 1..Len(pendingQ) : pendingQ[i][1] = t, pendingQ)

Stutter(t) == 
  /\ stuttering[t] > 0 
  /\ stuttering' = [stuttering EXCEPT ![t]= @-1] 
  /\ IF tstate[t] \in {"waiting", "exiting"} 
       THEN /\ pendingQ' = Append(pendingQ, <<t, IF tstate[t] = "waiting"
                                                      THEN "enter"
                                                      ELSE "exit">>)  
            /\ UNCHANGED iFace
       ELSE /\ UNCHANGED pendingQ
            /\ iFace' = [iFace EXCEPT !.rtn = <<t, "OK">>,
                                      !.rbit = (@+1) % 2   ]
  /\ UNCHANGED tstate

S_METry(t) == 
  /\ stuttering[t] = 0
  /\ METry(t) 
  /\ stuttering' = [stuttering EXCEPT ![t] = 1]
  /\ iFace' = [iFace EXCEPT !.arg = <<t, "enter">>,
                            !.abit = (@+1) % 2   ]
  /\ UNCHANGED pendingQ

S_MEEnterCS(t) == 
  /\ stuttering[t] = 0
  /\ MEEnterCS(t) 
  /\ stuttering' = [stuttering EXCEPT ![t] = 1]
  /\ pendingQ' = RemoveFromPendingQ(t) 
  /\ UNCHANGED iFace

S_MEExitCS(t) == 
  /\ stuttering[t] = 0
  /\ MEExitCS(t) 
  /\ stuttering' = [stuttering EXCEPT ![t] = 1]
  /\ iFace' = [iFace EXCEPT !.arg = <<t, "exit">>,
                            !.abit = (@+1) % 2     ]
  /\ UNCHANGED pendingQ

S_MEFinish(t) == 
  /\ stuttering[t] = 0
  /\ MEFinish(t) 
  /\ stuttering' = [stuttering EXCEPT ![t] = 1]
  /\ pendingQ' = RemoveFromPendingQ(t) 
  /\ UNCHANGED iFace

S_MENext == \E t \in Thread : 
               S_METry(t) \/ S_MEEnterCS(t) \/ S_MEExitCS(t) \/ S_MEFinish(t)
                \/ Stutter(t)

S_MEStarvationFree == 
   /\ S_MEInit 
   /\ [][S_MENext]_tstate 
   /\ \A t \in Thread : /\ WF_s_vars(S_MEFinish(t))
                        /\ SF_s_vars(S_MEEnterCS(t))
                        /\ WF_s_vars(Stutter(t))
-----------------------------------------------------------------------------
sstate == 
  LET incs(t) == \/ tstate[t] = "cs"
                 \/ /\ tstate[t] = "exiting"
                    /\ stuttering[t] = 1
  IN  IF \E t \in Thread : incs(t)
        THEN CHOOSE t \in Thread : incs(t)
        ELSE NotAThread

cstate ==
  [t \in Thread |-> 
    [ctl |-> CASE /\ tstate[t] \in {"cs", "noncs"}
                  /\ stuttering[t] = 0
                  -> "idle"    
             []   /\ tstate[t] \in {"waiting", "exiting"}
                  /\ stuttering[t] = 1
                  -> "calling"
             []   /\ tstate[t] \in {"waiting", "exiting"}
                  /\ stuttering[t] = 0
                  -> "pending"
             []   /\ tstate[t] \in {"cs", "noncs"}
                  /\ stuttering[t] = 1
                  -> "returning",
     val |-> CASE tstate[t] = "waiting" -> "enter"
             []   tstate[t] = "exiting" -> "exit"
             []   tstate[t] \in {"cs", "noncs"} -> "OK"]]

Bar == INSTANCE MCSMutex

TheSpec == Bar!MCSSpec
=============================================================================