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

GameChoose == /\ winner \in {"me", "you"} 
              /\ me' \in {"rock", "paper", "scissors"}
              /\ you' \in  {"rock", "paper", "scissors"}
              /\ winner' = "?"

GameWinner == /\ 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")
              /\ 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", "?"})

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