------------------------------ MODULE serie9_1 ------------------------------
EXTENDS TLC, Integers, Naturals
CONSTANT N

(*
--algorithm Bakery {
variables choosing = [ i \in 0..N-1 |-> FALSE],
          num = [ i \in 0..N-1 |-> 0],
          cs = [ i \in 0..N-1 |-> FALSE];
process (P \in  0..N-1)
variables j=0, max=0, p=0;
{

i1:choosing[self] := TRUE;
i21: while(j<N){
if (max > num[j]) {max:= num[j];};
 j:=j+1;
};
i2:num[self]:=max+1;
i3:choosing[self]:=FALSE;
p:=0;
ii:while(p<N){
i4:while((choosing[p]=TRUE)){skip;};
i5:while ((num[p]#0) /\ ((num[p]<num[self]) \/ ((num[p]=num[self]) /\ (p<self)) )){skip;};
p:=p+1;
};
cs:cs[self]:=TRUE;
i6: num[self]:=0;

};
    }




*)
\* BEGIN TRANSLATION
\* Label cs of process P at line 27 col 4 changed to cs_
VARIABLES choosing, num, cs, pc, j, max, p

vars == << choosing, num, cs, pc, j, max, p >>

ProcSet == (0..N-1)

Init == (* Global variables *)
        /\ choosing = [ i \in 0..N-1 |-> FALSE]
        /\ num = [ i \in 0..N-1 |-> 0]
        /\ cs = [ i \in 0..N-1 |-> FALSE]
        (* Process P *)
        /\ j = [self \in 0..N-1 |-> 0]
        /\ max = [self \in 0..N-1 |-> 0]
        /\ p = [self \in 0..N-1 |-> 0]
        /\ pc = [self \in ProcSet |-> "i1"]

i1(self) == /\ pc[self] = "i1"
            /\ choosing' = [choosing EXCEPT ![self] = TRUE]
            /\ pc' = [pc EXCEPT ![self] = "i21"]
            /\ UNCHANGED << num, cs, j, max, p >>

i21(self) == /\ pc[self] = "i21"
             /\ IF j[self]<N
                   THEN /\ IF max[self] > num[j[self]]
                              THEN /\ max' = [max EXCEPT ![self] = num[j[self]]]
                              ELSE /\ TRUE
                                   /\ max' = max
                        /\ j' = [j EXCEPT ![self] = j[self]+1]
                        /\ pc' = [pc EXCEPT ![self] = "i21"]
                   ELSE /\ pc' = [pc EXCEPT ![self] = "i2"]
                        /\ UNCHANGED << j, max >>
             /\ UNCHANGED << choosing, num, cs, p >>

i2(self) == /\ pc[self] = "i2"
            /\ num' = [num EXCEPT ![self] = max[self]+1]
            /\ pc' = [pc EXCEPT ![self] = "i3"]
            /\ UNCHANGED << choosing, cs, j, max, p >>

i3(self) == /\ pc[self] = "i3"
            /\ choosing' = [choosing EXCEPT ![self] = FALSE]
            /\ p' = [p EXCEPT ![self] = 0]
            /\ pc' = [pc EXCEPT ![self] = "ii"]
            /\ UNCHANGED << num, cs, j, max >>

ii(self) == /\ pc[self] = "ii"
            /\ IF p[self]<N
                  THEN /\ pc' = [pc EXCEPT ![self] = "i4"]
                  ELSE /\ pc' = [pc EXCEPT ![self] = "cs_"]
            /\ UNCHANGED << choosing, num, cs, j, max, p >>

i4(self) == /\ pc[self] = "i4"
            /\ IF (choosing[p[self]]=TRUE)
                  THEN /\ TRUE
                       /\ pc' = [pc EXCEPT ![self] = "i4"]
                  ELSE /\ pc' = [pc EXCEPT ![self] = "i5"]
            /\ UNCHANGED << choosing, num, cs, j, max, p >>

i5(self) == /\ pc[self] = "i5"
            /\ IF (num[p[self]]#0) /\ ((num[p[self]]<num[self]) \/ ((num[p[self]]=num[self]) /\ (p[self]<self)) )
                  THEN /\ TRUE
                       /\ pc' = [pc EXCEPT ![self] = "i5"]
                       /\ p' = p
                  ELSE /\ p' = [p EXCEPT ![self] = p[self]+1]
                       /\ pc' = [pc EXCEPT ![self] = "ii"]
            /\ UNCHANGED << choosing, num, cs, j, max >>

cs_(self) == /\ pc[self] = "cs_"
             /\ cs' = [cs EXCEPT ![self] = TRUE]
             /\ pc' = [pc EXCEPT ![self] = "i6"]
             /\ UNCHANGED << choosing, num, j, max, p >>

i6(self) == /\ pc[self] = "i6"
            /\ num' = [num EXCEPT ![self] = 0]
            /\ pc' = [pc EXCEPT ![self] = "Done"]
            /\ UNCHANGED << choosing, cs, j, max, p >>

P(self) == i1(self) \/ i21(self) \/ i2(self) \/ i3(self) \/ ii(self)
              \/ i4(self) \/ i5(self) \/ cs_(self) \/ i6(self)

Next == (\E self \in 0..N-1: P(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

Qmutex == \A u \in 0..N-1: cs[u]=TRUE => \A v \in 0..N-1:v#u => cs[v]=FALSE
Qreachable == cs[0] # TRUE

=============================================================================
\* Modification History
\* Last modified Wed Dec 02 09:49:27 CET 2015 by garnier34u
\* Created Wed Dec 02 08:47:46 CET 2015 by garnier34u