tictactoe.tla

EXTENDS Integers
CONSTANT EMPTY

(*
The basic model is to map positions in a sequence to
the squares on a tic-tac-toe board, as

1 | 2 | 3
---------
4 | 5 | 6
---------
7 | 8 | 9

*)

SQUARES == 1..9

(*--algorithm tictactoe

variables board = [s \in SQUARES |-> EMPTY],
                  current_letter \in {"X", "O"};
          
define
    BoardFull == \A square \in SQUARES: board[square] /= EMPTY
    EmptySquares == {square \in SQUARES: board[square] = EMPTY}
    WinningCombos == { <<1, 2, 3>>,
                       <<4, 5, 6>>,
                       <<7, 8, 9>>,
                       <<1, 5, 9>>,
                       <<3, 5, 7>>,
                       <<1, 4, 7>>,
                       <<2, 5, 8>>,
                       <<3, 6, 9>>}
    ComboAsSet(combo) == {combo[square] : square \in 1..3}                   
    Winner(Player) == \E combo \in WinningCombos :
                        \A square1, square2 \in ComboAsSet(combo):
                            /\ board[square1] = board[square2]
                            /\ board[square1] = Player
                    
    XWins == Winner("X")
    OWins == Winner("O")
    SomeWinner == \E letter \in {"X", "O"} : Winner(letter)
end define;

begin
    while ~BoardFull /\ ~SomeWinner do
        with chosen_square \in EmptySquares do
            board[chosen_square] := current_letter;
        end with;
        if current_letter = "X" then
            current_letter := "O";
        else
            current_letter := "X";
        end if
    end while;
end algorithm;*)

Try

(*--algorithm tictactoe
+(**)

Then it will stop treating the pluscal as a comment

- BoardFull == \A square \in SQUARES: board[square] /= EMPTY
EmptySquares == {square \in SQUARES: board[square] = EMPTY}
+ BoardFull == EmptySquares = {}

You should probably use a set of sets instead of a set of seqs for WinningCombo