---------------------------- MODULE AtomicBakery ---------------------------- 
EXTENDS Naturals

CONSTANT N 
ASSUME N > 1

Thread == 1..N

VARIABLE num, pc, d1Done, d2Done, w1Done

vars == <<num, pc, w1Done, dDone, eDone>>
-----------------------------------------------------------------------------
ABInit == /\ num    = [t \in Thread |-> 0]
          /\ pc     = [t \in Thread |-> "noncs"]
          /\ w1Done = [t \in Thread |-> {}]
          /\ dDone  = [t \in Thread |-> {}]
          /\ eDone  = [t \in Thread |-> {}]

ABTypeOK == /\ num \in [Thread -> Nat]
            /\ pc \in [Thread -> {"noncs", "w1", "w2", "w3", "cs", "exiting"}]
            /\ w1Done \in [Thread -> SUBSET Thread]
            /\ dDone  \in [Thread -> SUBSET Thread]
            /\ eDone  \in [Thread -> SUBSET Thread]
-----------------------------------------------------------------------------
GoTo(t, loc1, loc2) == /\ tstate[t] = loc1
                       /\ tstate' = [tstate EXCEPT ![t] = loc2]

ABSetNum(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}]

ABWaitFor(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

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

ABFinish(t) ==
  /\ GoTo(t, "exiting", "noncs")
  /\ num' = [num EXCEPT ![t] = 0]
  /\ UNCHANGED waitingFor
                     
ABNext == 
  \E t \in Thread : \/ ABSetNum(t)
                    \/ \E i \in Thread \ {t} : ABWaitFor(t, i) 
                    \/ ABExitCS(t)
                    \/ ABFinish(t)

ABEnterOrFinish == 
  \E t \in Thread : \/ \E i \in Thread \ {t} : ABWaitFor(t, i) 
                    \/ ABFinish(t)

ABSpec == ABInit /\ [][ABNext]_vars  /\ WF_vars(ABEnterOrFinish)
=============================================================================