----------------- MODULE TTT -----------------
VARIABLES
  turn, next, s0, s1, s2, s3, s4, s5, s6, s7, s8, winner 
----------------------------------------------

TTTInit == /\ turn = "O"
           /\ s0 = " "
           /\ s1 = " "
           /\ s2 = " "
           /\ s3 = " "
           /\ s4 = " "
           /\ s5 = " "
           /\ s6 = " "
           /\ s7 = " "
           /\ s8 = " "
           /\ winner = "?"
           /\ next = "move"

TTTMoveO == /\ turn = "O"
            /\ next = "move"
            /\ \/ (s0 = " " /\ s0' = "O" /\ UNCHANGED <<s1, s2, s3, s4, s5, s6, s7, s8>>)
               \/ (s1 = " " /\ s1' = "O" /\ UNCHANGED <<s0, s2, s3, s4, s5, s6, s7, s8>>)
               \/ (s2 = " " /\ s2' = "O" /\ UNCHANGED <<s0, s1, s3, s4, s5, s6, s7, s8>>)
               \/ (s3 = " " /\ s3' = "O" /\ UNCHANGED <<s0, s1, s2, s4, s5, s6, s7, s8>>)
               \/ (s4 = " " /\ s4' = "O" /\ UNCHANGED <<s0, s1, s2, s3, s5, s6, s7, s8>>)
               \/ (s5 = " " /\ s5' = "O" /\ UNCHANGED <<s0, s1, s2, s3, s4, s6, s7, s8>>)
               \/ (s6 = " " /\ s6' = "O" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s7, s8>>)
               \/ (s7 = " " /\ s7' = "O" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s6, s8>>)
               \/ (s8 = " " /\ s8' = "O" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s6, s7>>)
            /\ turn' = "X"
            /\ UNCHANGED winner
            /\ next' = "winner"

TTTMoveX == /\ turn = "X"
            /\ next = "move"
            /\ \/ (s0 = " " /\ s0' = "X" /\ UNCHANGED <<s1, s2, s3, s4, s5, s6, s7, s8>>)
               \/ (s1 = " " /\ s1' = "X" /\ UNCHANGED <<s0, s2, s3, s4, s5, s6, s7, s8>>)
               \/ (s2 = " " /\ s2' = "X" /\ UNCHANGED <<s0, s1, s3, s4, s5, s6, s7, s8>>)
               \/ (s3 = " " /\ s3' = "X" /\ UNCHANGED <<s0, s1, s2, s4, s5, s6, s7, s8>>)
               \/ (s4 = " " /\ s4' = "X" /\ UNCHANGED <<s0, s1, s2, s3, s5, s6, s7, s8>>)
               \/ (s5 = " " /\ s5' = "X" /\ UNCHANGED <<s0, s1, s2, s3, s4, s6, s7, s8>>)
               \/ (s6 = " " /\ s6' = "X" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s7, s8>>)
               \/ (s7 = " " /\ s7' = "X" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s6, s8>>)
               \/ (s8 = " " /\ s8' = "X" /\ UNCHANGED <<s0, s1, s2, s3, s4, s5, s6, s7>>)
            /\ turn' = "O"
            /\ UNCHANGED winner
            /\ next' = "winner"

TTTWinner == /\ winner = "?"
             /\ next = "winner"
             /\ \/ /\ s0 = s1
                   /\ s1 = s2
                   /\ s0 # " "
                   /\ winner' = IF s0 = "X" THEN "me" ELSE "you"
                \/ /\ s3 = s4
                   /\ s4 = s5
                   /\ s3 # " "
                   /\ winner' = IF s3 = "X" THEN "me" ELSE "you"
                \/ /\ s6 = s7
                   /\ s7 = s8
                   /\ s6 # " "
                   /\ winner' = IF s6 = "X" THEN "me" ELSE "you"
                \/ /\ s0 = s3
                   /\ s3 = s6
                   /\ s0 # " "
                   /\ winner' = IF s0 = "X" THEN "me" ELSE "you"
                \/ /\ s1 = s4
                   /\ s4 = s7
                   /\ s1 # " "
                   /\ winner' = IF s1 = "X" THEN "me" ELSE "you"
                \/ /\ s2 = s5
                   /\ s5 = s8
                   /\ s2 # " "
                   /\ winner' = IF s2 = "X" THEN "me" ELSE "you"
                \/ /\ s0 = s4
                   /\ s4 = s8
                   /\ s0 # " "
                   /\ winner' = IF s0 = "X" THEN "me" ELSE "you"
                \/ /\ s2 = s4
                   /\ s4 = s6
                   /\ s2 # " "
                   /\ winner' = IF s2 = "X" THEN "me" ELSE "you"
             /\ UNCHANGED <<turn, s0, s1, s2, s3, s4, s5, s6, s7, s8>>
             /\ next' = IF winner' = "?" THEN "move" ELSE "winner"

TTTNext == TTTMoveO \/ TTTMoveX \/ TTTWinner 
----------------------------------------------
TTTSpec == TTTInit /\ [][TTTNext]_<<winner, s0, s1, s2, s3, s4, s5, s6, s7, s8>>
==============================================