[tlaplus] Specification for tic-tac-toe in PlusCal

Hi,

As an exercise to help me learn PlusCal, I've written an spec for tic-tac-toe. I would appreciate any comments to make this spec better.

Thanks,

David

------------------------------- MODULE game3 -------------------------------

EXTENDS Sequences, Integers, FiniteSets, TLC

(*--algorithm TicTacToe

variables
    board = <<"", "", "", "", "", "", "", "", "">>,
    square = 0,
    possibleSquares = 1..9,
    usedSquares = [X |-> {}, O |-> {}],
    xIsNext = TRUE,
    gameIsOver = FALSE,
    winningPositions = {{1, 2, 3}, {1, 4, 7}, {1, 5, 9}, {2, 5, 8}, {3, 5, 7}, {3, 6, 9}, {4, 5, 6}, {7, 8, 9}},
    winner = "";

macro makeMove(piece) begin

    board[square] := piece;
    usedSquares[piece] := usedSquares[piece] \union { square };

    if Cardinality({ position \in winningPositions : position \ usedSquares[piece] = {} }) = 1 then
        winner := piece;
    end if;

    if winner /= "" then
        gameIsOver := TRUE;
    else
        gameIsOver := possibleSquares \ (usedSquares.X \union usedSquares.O) = {};
    end if;

end macro;

fair process player \in { "X", "O" }
begin
    Play:
        while ~gameIsOver do

            if self = "X" then
                await xIsNext;
            else
                await ~xIsNext;
            end if;

            with openSquare \in possibleSquares \ (usedSquares.X \union usedSquares.O) do
                square := openSquare
            end with;

            makeMove(self);
            xIsNext := ~xIsNext;

            assert Cardinality(usedSquares.X) - Cardinality(usedSquares.O) \in { 0, 1 };
            assert Cardinality(usedSquares.X) = Len(SelectSeq(board, LAMBDA x : x = "X"));
            assert Cardinality(usedSquares.O) = Len(SelectSeq(board, LAMBDA x : x = "O"));
        end while
end process

end algorithm *)