---------------------------- MODULE SimpleBakery ---------------------------- 
EXTENDS Naturals

CONSTANT N 
ASSUME N > 1

Thread == 1..N

VARIABLE num, tstate, waitingFor

vars == <<num, tstate, waitingFor>>
-----------------------------------------------------------------------------
SBInit == /\ num = [t \in Thread |-> 0]
          /\ tstate = [t \in Thread |-> "noncs"]
          /\ waitingFor = [t \in Thread |-> {}]

SBTypeOK == /\ num \in [Thread -> Nat]
            /\ tstate \in [Thread -> {"noncs", "waiting", "cs", "exiting"}]
            /\ waitingFor \in [Thread -> SUBSET Thread]
-----------------------------------------------------------------------------
GoTo(t, loc1, loc2) == /\ tstate[t] = loc1
                       /\ tstate' = [tstate EXCEPT ![t] = loc2]

SBSetNum(t) == 
  LET max[i \in Thread] ==  IF i = 1 THEN num[1]
                                     ELSE IF num[i] > max[i-1] THEN num[i]
                                                               ELSE max[i-1]
      maxNum == max[N]
  IN  /\ GoTo(t, "noncs", "waiting")
      /\ num' = [num EXCEPT ![t] = 1 + maxNum]
      /\ waitingFor' = [waitingFor EXCEPT ![t] = Thread \ {t}]

SBWaitFor(t, i) == 
  /\ tstate[t] = "waiting"
  /\ i \in waitingFor[t]
  /\ (num[i] = 0) \/ (num[t] < num[i])
  /\ waitingFor' = [waitingFor EXCEPT ![t] = @ \ {i}]
  /\ tstate' = IF waitingFor'[t] = { } THEN [tstate EXCEPT ![t] = "cs"]
                                       ELSE tstate
  /\ UNCHANGED num

SBExitCS(t) ==
  /\ GoTo(t, "cs", "exiting")
  /\ UNCHANGED <<num, waitingFor>>

SBFinish(t) ==
  /\ GoTo(t, "exiting", "noncs")
  /\ num' = [num EXCEPT ![t] = 0]
  /\ UNCHANGED waitingFor
                     
SBNext == 
  \E t \in Thread : \/ SBSetNum(t)
                    \/ \E i \in Thread \ {t} : SBWaitFor(t, i) 
                    \/ SBExitCS(t)
                    \/ SBFinish(t)

SBEnterOrFinish == 
  \E t \in Thread : \/ \E i \in Thread \ {t} : SBWaitFor(t, i) 
                    \/ SBFinish(t)

SBSpec == SBInit /\ [][SBNext]_vars  /\ WF_vars(SBEnterOrFinish)
=============================================================================