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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.