Specification for tic-tac-toe in PlusCal

[David Jimenez]

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 *)