------------------------------ MODULE serie7_4 ------------------------------
EXTENDS Naturals, Integers, TLC
CONSTANTS flag, turn, pc1, pc2

al0l1 ==
    /\ pc1="l0" /\ pc1' = "l1"
    /\ flag' = [flag EXCEPT![0]=TRUE]
    /\ UNCHANGED <<pc2, turn>>

al1l2 ==
    /\ pc1="l1" /\ pc1' = "l2"
    /\ turn' = 1
    /\ UNCHANGED <<pc2, flag>>

al2l2 ==
    /\ pc1="l2"
    /\ flag[1]=TRUE /\ turn = 1
    /\ UNCHANGED <<turn, pc1, pc2, flag>>

al2l3 ==
    /\ pc1="l2"
    /\ ~flag[1]=TRUE /\ turn = 1
    /\ pc1'="l3"
    /\ UNCHANGED <<pc2, flag, turn>>

al3l0 ==
    /\ pc2="l3" /\ pc2' = "l0"
    /\ flag' = [flag EXCEPT![1]=FALSE]
    /\ UNCHANGED <<pc1, turn>>

Next1 == al0l1 \/ al1l2 \/ al2l3 \/ al3l0

am0m1 ==
    /\ pc2="m0" /\ pc2' = "m1"
    /\ flag' = [flag EXCEPT![1]=TRUE]
    /\ UNCHANGED <<pc1, turn>>

am1m2 ==
    /\ pc2="m1" /\ pc2' = "m2"
    /\ turn' = 0
    /\ UNCHANGED <<pc1, flag>>

am2m2 ==
    /\ pc2="m2"
    /\ flag[0]=TRUE /\ turn = 0
    /\ UNCHANGED <<turn, pc1, pc2, flag>>

am2m3 ==
    /\ pc2="m2"
    /\ ~flag[0]=TRUE /\ turn = 0
    /\ pc2'="m3"
    /\ UNCHANGED <<pc1, flag, turn>>

am3m0 ==
    /\ pc2="m3" /\ pc2' = "m0"
    /\ flag' = [flag EXCEPT![1]=FALSE]
    /\ UNCHANGED <<pc1, turn>>

Next2 == am0m1 \/ am1m2 \/ am2m3 \/ am3m0

Next == Next1 \/ Next2

Init == pc1="l0" /\ pc2 ="m0" /\ turn = FALSE /\ flag = [p \in {0,1} |-> FALSE ]

Qmutex == ~(pc1="l3" /\ pc2="m3")

=============================================================================
\* Modification History
\* Last modified Thu Nov 26 09:50:15 CET 2015 by garnier34u
\* Created Thu Nov 26 09:13:09 CET 2015 by garnier34u