---------------- MODULE Alternate ----------------
\*************************************************
\*
\*   int x = 0
\*   while (true) {
\*      a1: await (x == 0);
\*      a2: x = 1
\*      a3: (outside of CS)
\*      }
\*|| while (true) {
\*      b1: await (x == 1)
\*      b2: x = 0
\*      b3: (outside of CS)
\*      }
\*
\*************************************************
EXTENDS Naturals
VARIABLES pc, x

AGoTo(from, to) == /\ pc.a = from
                   /\ pc' = [a |-> to, b |-> pc.b]

BGoTo(from, to) == /\ pc.b = from
                   /\ pc' = [a |-> pc.a, b |-> to]

--------------------------------------------------
AlternateInit == /\ pc = [a |-> 1, b |-> 1]
                 /\ x = 0

AlternateA1 == /\ AGoTo(1, 2)
               /\ x = 0
               /\ UNCHANGED x

AlternateA2 == /\ AGoTo(2, 3)
               /\ x' = 1

AlternateA3 == /\ AGoTo(3, 1)
               /\ UNCHANGED x

AlternateB1 == /\ BGoTo(1, 2)
               /\ x = 1
               /\ UNCHANGED x

AlternateB2 == /\ BGoTo(2, 3)
               /\ x' = 0

AlternateB3 == /\ BGoTo(3, 1)
               /\ UNCHANGED x

---------------------------------------------------
AlternateNext == \/ AlternateA1 \/ AlternateA2 \/ AlternateA3
                 \/ AlternateB1 \/ AlternateB2 \/ AlternateB3

AlternateSpec == /\ AlternateInit
                 /\ [][AlternateNext]_<<x, pc>>
                 /\ WF_<<x, pc>>(AlternateA1)
                 /\ WF_<<x, pc>>(AlternateA2)
\*               /\ WF_<<x, pc>>(AlternateA3)
                 /\ WF_<<x, pc>>(AlternateB1)
                 /\ WF_<<x, pc>>(AlternateB2)
\*               /\ WF_<<x, pc>>(AlternateB3)

AlternateTypeOK == /\ x \in 0..1
                   /\ pc \in [a: 1..3, b: 1..3]

AlternateIsMutex == pc # [a |-> 2, b |-> 2]

AlternateIsFair == /\ (pc.a = 1) ~> (pc.a = 2)
                   /\ (pc.b = 1) ~> (pc.b = 2)

THEOREM AlternateSpec => []AlternateTypeOK
THEOREM AlternateSpec => []AlternateIsMutex
THEOREM AlternateSpec => AlternateIsFair
==================================================