------------------ MODULE Game -----------------
VARIABLE me, you, next, winner
------------------------------------------------
GameInit == /\ (me \in {"rock", "paper", "scissors"})
            /\ (you \in {"rock", "paper", "scissors"})
            /\ winner = "?"
            /\ next = "winner"

GameChoose == /\ next = "choose"
              /\ \/ /\ winner  = "?"
                    /\ me' \in {"rock", "paper", "scissors"}
                    /\ you' \in  {"rock", "paper", "scissors"}
                    /\ UNCHANGED winner
                 \/ /\ winner \in {"me", "you"}
                    /\ UNCHANGED <<me, you, winner>>
              /\ next' = "winner"

GameWinner == /\ winner = "?"
              /\ next = "winner"
              /\ \/ (me = "rock" /\ you = "paper" /\ winner' = "you")
                 \/ (me = "paper" /\ you = "scissors" /\ winner' = "you")
                 \/ (me = "scissors" /\ you = "rock" /\ winner' = "you")
                 \/ (me = "rock" /\ you = "scissors" /\ winner' = "me")
                 \/ (me = "scissors" /\ you = "paper" /\ winner' = "me")
                 \/ (me = "paper" /\ you = "rock" /\ winner' = "me")
                 \/ (me = you /\ UNCHANGED winner /\ next' = "choose")
              /\ UNCHANGED <<me, you>>

                

GameNext == GameChoose \/ GameWinner 
------------------------------------------------
GameSpec == GameInit /\ [][GameNext]_<<me, you, winner>>

GameInvariant == /\ (me \in {"rock", "paper", "scissors"})
                 /\ (you \in {"rock", "paper", "scissors"})
                 /\ (winner \in {"me", "you", "?"})

THEOREM GameSpec => []GameInvariant
================================================