/********************************************************************* * A simple model of a tic-tac-toe game (noughts and crosses)
*********************************************************************/
module XO exportsall definitions values
SIZE:nat1 = 3; -- The size of the board (3x3)
MAX:nat1 = SIZE * SIZE; -- The maximum number of moves
types-- Types composed of primitives, plus invariants
Player = <NOUGHT> | <CROSS>; -- Just two players
Pos :: -- A position for a move
row : nat1
col : nat1 inv p ==
p.row <= SIZE and p.col <= SIZE; -- Row/col must be on the board
Game = map Pos to Player -- A game (who has moved where) inv g == forall p1, p2 : Player & -- No player is ever more than one move ahead carddom (g :> {p1}) - carddom (g :> {p2}) inset {-1, 0, 1}
values
S:setofnat1 = {1, ..., SIZE};
winningLines = dunion-- Sets of Pos for winning lines
{
{{ mk_Pos(r, c) | c inset S } | r inset S }, -- All rows
{{ mk_Pos(r, c) | r inset S } | c inset S }, -- All columns
{{ mk_Pos(x, x) | x inset S }}, -- Diagnonal
{{ mk_Pos(x, SIZE-x+1) | x inset S }} -- Other diagonal
};
functions-- Definition of various play "states" of a game or a player.
hasWon: Game * Player -> bool
hasWon(g, p) == let moves = movesForPlayer(g, p) in exists line inset winningLines &
line subset moves;
whoWon: Game -> Player
whoWon(g) == iota p:Player & hasWon(g, p) pre isWon(g);
isDraw: Game -> bool
isDraw(g) == not isWon(g) and moveCountLeft(g) = 0;
isUnfinished: Game -> bool
isUnfinished(g) == not isWon(g) andnot isDraw(g);
movesSoFar: Game -> setof Pos
movesSoFar(g) == dom g;
moveCountSoFar: Game -> nat
moveCountSoFar(g) == card movesSoFar(g);
moveCountLeft: Game -> nat
moveCountLeft(g) ==
MAX - moveCountSoFar(g);
movesForPlayer: Game * Player -> setof Pos
movesForPlayer(g, p) == dom (g :> {p});
values
PLAYERS = { p | p:Player }; -- The set of all Players
types-- These types are to do with moves and playing
Moves = seqof Pos -- A legal game play sequence inv moves == len moves = cardelems moves and-- Has no duplicated moves len moves > card PLAYERS * (SIZE - 1) and-- Has minimum moves to win len moves <= MAX; -- Hasn't too many moves
PlayOrder = seq1of Player -- The order of play of the players inv order == len order = cardelems order and-- No duplicates in the list elems order = PLAYERS -- Order contains all players
state Sigma of-- Sigma is just a convention for the name of a system state
game : Game -- The game board, initialized by the play operation end
operations-- Processes that use the functions above to define how to play
move: Player * Pos ==> ()
move(p, pos) ==
game(pos) := p pre pos notinset movesSoFar(game) and
moveCountLeft(game) > 0 post game = game~ munion {pos |-> p} and
moveCountSoFar(game) = moveCountSoFar(game~) + 1;
play: PlayOrder * Moves ==> Player | <DRAW> | <UNFINISHED>
play(playorder, moves) ==
( dcl order:PlayOrder := playorder; -- hd order is always next to play
game := {|->};
for m in moves do let player = hd order in
(
move(player, m);
if isWon(game) then return whoWon(game) elseif isDraw(game) then return <DRAW> else
order := tl order ^ [player]
);
return <UNFINISHED>
) postifRESULT = <DRAW> then isDraw(game) elseifRESULT = <UNFINISHED> then isUnfinished(game) elseRESULT = whoWon(game);
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
