------------------------------ MODULE serie8_1 ------------------------------
EXTENDS Naturals, Integers, TLC

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

process (P=0)
{ 
    start0: flag[0]:=TRUE;
    inturn0: turn:=1;
    wait: while(flag[1]=TRUE /\ turn=1){
        p:=p+1;
    };
    incs0: x:=x+1;
    outcs0: flag[0]:=FALSE;
    goto start0;
};

process (Q=1)
{
    start1: flag[1]:=TRUE;
    inturn1: turn:=0;
    wait:while(flag[0]=TRUE /\ turn=0){
        p:=p+1;
    };
    incs1: x:=x+1;
    outcs1: flag[1]:=FALSE;
    goto start1;
}   
}
*)
\* BEGIN TRANSLATION
\* Label wait of process P at line 15 col 11 changed to wait_
VARIABLES x, p, flag, turn, pc

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

ProcSet == {0} \cup {1}

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

start0 == /\ pc[0] = "start0"
          /\ flag' = [flag EXCEPT ![0] = TRUE]
          /\ pc' = [pc EXCEPT ![0] = "inturn0"]
          /\ UNCHANGED << x, p, turn >>
 
inturn0 == /\ pc[0] = "inturn0"
           /\ turn' = 1
           /\ pc' = [pc EXCEPT ![0] = "wait_"]
           /\ UNCHANGED << x, p, flag >>

wait_ == /\ pc[0] = "wait_"
         /\ IF flag[1]=TRUE /\ turn=1
               THEN /\ p' = p+1
                    /\ pc' = [pc EXCEPT ![0] = "wait_"]
               ELSE /\ pc' = [pc EXCEPT ![0] = "incs0"]
                    /\ p' = p
         /\ UNCHANGED << x, flag, turn >>

incs0 == /\ pc[0] = "incs0"
         /\ x' = x+1
         /\ pc' = [pc EXCEPT ![0] = "outcs0"]
         /\ UNCHANGED << p, flag, turn >>

outcs0 == /\ pc[0] = "outcs0"
          /\ flag' = [flag EXCEPT ![0] = FALSE]
          /\ pc' = [pc EXCEPT ![0] = "start0"]
          /\ UNCHANGED << x, p, turn >>

P == start0 \/ inturn0 \/ wait_ \/ incs0 \/ outcs0

start1 == /\ pc[1] = "start1"
          /\ flag' = [flag EXCEPT ![1] = TRUE]
          /\ pc' = [pc EXCEPT ![1] = "inturn1"]
          /\ UNCHANGED << x, p, turn >>

inturn1 == /\ pc[1] = "inturn1"
           /\ turn' = 0
           /\ pc' = [pc EXCEPT ![1] = "wait"]
           /\ UNCHANGED << x, p, flag >>

wait == /\ pc[1] = "wait"
        /\ IF flag[0]=TRUE /\ turn=0
              THEN /\ p' = p+1
                   /\ pc' = [pc EXCEPT ![1] = "wait"]
              ELSE /\ pc' = [pc EXCEPT ![1] = "incs1"]
                   /\ p' = p
        /\ UNCHANGED << x, flag, turn >>

incs1 == /\ pc[1] = "incs1"
         /\ x' = x+1
         /\ pc' = [pc EXCEPT ![1] = "outcs1"]
         /\ UNCHANGED << p, flag, turn >>

outcs1 == /\ pc[1] = "outcs1"
          /\ flag' = [flag EXCEPT ![1] = FALSE]
          /\ pc' = [pc EXCEPT ![1] = "start1"]
          /\ UNCHANGED << x, p, turn >>

Q == start1 \/ inturn1 \/ wait \/ incs1 \/ outcs1

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:37:45 CET 2015 by garnier34u
\* Created Fri Nov 27 13:31:01 CET 2015 by garnier34u