------------------------------ MODULE serie8_2 ------------------------------
EXTENDS Naturals, Integers, TLC


(*
-termination
-wfNext
--algorithm mutex{
  variables turn=1,p=0,x=0, flag=[i \in 0..1 |-> FALSE],flagP=0,flagQ=0;

   
    process (P=0)
    {
        start0:while(x \leq 10) {
            flag[0] := flag[0]+1;
            x:=x+1;
        };
        
        print<<"flag[0]:", flag[0]>>;
    };
    
    process (Q=1)
    {
        start1:while(x \leq 10) {
            x:=x+1;
            flag[1]:=flag[1]+1;
        };
        
        print<<"flag[1]:", flag[1]>>;
    };
    

}
*)
\* BEGIN TRANSLATION
VARIABLES turn, p, x, flag, flagP, flagQ, pc

vars == << turn, p, x, flag, flagP, flagQ, pc >>

ProcSet == {0} \cup {1}

Init == (* Global variables *)
        /\ turn = 1
        /\ p = 0
        /\ x = 0
        /\ flag = [i \in 0..1 |-> FALSE]
        /\ flagP = 0
        /\ flagQ = 0
        /\ pc = [self \in ProcSet |-> CASE self = 0 -> "start0"
                                        [] self = 1 -> "start1"]

start0 == /\ pc[0] = "start0"
          /\ IF x \leq 10
                THEN /\ flag' = [flag EXCEPT ![0] = flag[0]+1]
                     /\ x' = x+1
                     /\ pc' = [pc EXCEPT ![0] = "start0"]
                ELSE /\ PrintT(<<"flag[0]:", flag[0]>>)
                     /\ pc' = [pc EXCEPT ![0] = "Done"]
                     /\ UNCHANGED << x, flag >>
          /\ UNCHANGED << turn, p, flagP, flagQ >>

P == start0

start1 == /\ pc[1] = "start1"
          /\ IF x \leq 10
                THEN /\ x' = x+1
                     /\ flag' = [flag EXCEPT ![1] = flag[1]+1]
                     /\ pc' = [pc EXCEPT ![1] = "start1"]
                ELSE /\ PrintT(<<"flag[1]:", flag[1]>>)
                     /\ pc' = [pc EXCEPT ![1] = "Done"]
                     /\ UNCHANGED << x, flag >>
          /\ UNCHANGED << turn, p, flagP, flagQ >>

Q == start1

Next == P \/ Q
           \/ (* 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

=============================================================================
\* Modification History
\* Last modified Fri Nov 27 14:38:07 CET 2015 by garnier34u
\* Created Fri Nov 27 14:38:00 CET 2015 by garnier34u