--------------------------- MODULE MCSimpleBakery --------------------------- 
EXTENDS SimpleBakery

CONSTANT MaxNum

MCConstraint == \A t \in Thread : num[t] < MaxNum

Bar == INSTANCE MutualExclusion 
Bar_MEStarvationFree == Bar!MEStarvationFree

SBInductiveInvariant ==
   \A t1 \in Thread :
     /\ (tstate[t1] # "noncs") => (num[t1] > 0)
     /\ \A t2 \in Thread \ {t1} :
           (\/ tstate[t1] = "cs"
            \/ (tstate[t1]= "waiting") /\ (t2 \notin waitingFor[t1]))
            => (num[t2]=0) \/ (num[t2]>num[t1])

\* MCTestInvSpec == (SBTypeOK /\ SBInductiveInvariant )  /\ [][SBNext]_vars
\* MCNat == 0..MaxNum
=============================================================================