---------------- MODULE Peterson ----------------
\************************************************
\*
\*   int a = 0, b = 0
\*   id turn = either "a" or "b"
\*   while (true) {
\*      a1: a = 1
\*      a2: turn = "b"
\*      a3: await(b == 0 || turn = "a")
\*      a4: a = 0
\*      a5: (outside of CS)
\*      }
\*|| while (true) {
\*      b1: b = 1
\*      b2: turn = "a"
\*      b3: await(a == 0 || turn = "b")
\*      b4: b = 0
\*      b5: (outside of CS)
\*      }
\*
\************************************************
EXTENDS Naturals
VARIABLES pc, turn, a, b

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

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

-------------------------------------------------
PetersonInit == /\ pc = [a |-> 1, b |-> 1]
                /\ turn \in {"a", "b"}
                /\ a = 0
                /\ b = 0

PetersonA1 == /\ AGoTo(1, 2)
              /\ a' = 1
              /\ UNCHANGED <<b, turn>>

PetersonA2 == /\ AGoTo(2, 3)
              /\ turn' = "b"
              /\ UNCHANGED <<a, b>>

PetersonA3 == /\ AGoTo(3, 4)
              /\ (b = 0) \/ (turn = "a")
              /\ UNCHANGED <<a, b, turn>>

PetersonA4 == /\ AGoTo(4, 5)
              /\ a' = 0
              /\ UNCHANGED <<b, turn>>

PetersonA5 == /\ AGoTo(5, 1)
              /\ UNCHANGED <<a, b, turn>>

PetersonB1 == /\ BGoTo(1, 2)
              /\ b' = 1
              /\ UNCHANGED <<a, turn>>

PetersonB2 == /\ BGoTo(2, 3)
              /\ turn' = "a"
              /\ UNCHANGED <<a, b>>

PetersonB3 == /\ BGoTo(3, 4)
              /\ (a = 0) \/ (turn = "b")
              /\ UNCHANGED <<a, b, turn>>

PetersonB4 == /\ BGoTo(4, 5)
              /\ b' = 0
              /\ UNCHANGED <<a, turn>>

PetersonB5 == /\ BGoTo(5, 1)
              /\ UNCHANGED <<a, b, turn>>

-------------------------------------------------
PetersonNext == \/ PetersonA1 \/ PetersonA2 \/ PetersonA3
                \/ PetersonA4 \/ PetersonA5
                \/ PetersonB1 \/ PetersonB2 \/ PetersonB3
                \/ PetersonB4 \/ PetersonB5

PetersonSpec == /\ PetersonInit
                /\ [][PetersonNext]_<<a, b, turn, pc>>
                /\ WF_<<a, b, turn, pc>>(PetersonA1)
                /\ WF_<<a, b, turn, pc>>(PetersonA2)
                /\ WF_<<a, b, turn, pc>>(PetersonA3)
                /\ WF_<<a, b, turn, pc>>(PetersonA4)
                /\ WF_<<a, b, turn, pc>>(PetersonB1)
                /\ WF_<<a, b, turn, pc>>(PetersonB2)
                /\ WF_<<a, b, turn, pc>>(PetersonB3)
                /\ WF_<<a, b, turn, pc>>(PetersonB4)

PetersonTypeOK == /\ turn \in {"a", "b"}
                  /\ a \in 0..1
                  /\ b \in 0..1
                  /\ pc \in [a: 1..5, b: 1..5]

PetersonIsMutex == pc # [a |-> 4, b |-> 4]

PetersonIsFair == /\ (pc.a = 1) ~> (pc.a = 4)
                  /\ (pc.b = 1) ~> (pc.b = 4)

THEOREM PetersonSpec => []PetersonTypeOK
THEOREM PetersonSpec => []PetersonIsMutex
THEOREM PetersonSpec => PetersonIsFair
=================================================