|
/*********************************************************************
* A simple model of a tic-tac-toe game (noughts and crosses)
*********************************************************************/
module XO
exports all
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
card dom (g :> {p1}) - card dom (g :> {p2}) in set {-1, 0, 1}
values
S:set of nat1 = {1, ..., SIZE};
winningLines = dunion -- Sets of Pos for winning lines
{
{{ mk_Pos(r, c) | c in set S } | r in set S }, -- All rows
{{ mk_Pos(r, c) | r in set S } | c in set S }, -- All columns
{{ mk_Pos(x, x) | x in set S }}, -- Diagnonal
{{ mk_Pos(x, SIZE-x+1) | x in set 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 in set winningLines &
line subset moves;
whoWon: Game -> Player
whoWon(g) ==
iota p:Player & hasWon(g, p)
pre isWon(g);
isWon: Game -> bool
isWon(g) ==
exists1 p:Player & hasWon(g, p);
isDraw: Game -> bool
isDraw(g) ==
not isWon(g) and moveCountLeft(g) = 0;
isUnfinished: Game -> bool
isUnfinished(g) ==
not isWon(g) and not isDraw(g);
movesSoFar: Game -> set of Pos
movesSoFar(g) ==
dom g;
moveCountSoFar: Game -> nat
moveCountSoFar(g) ==
card movesSoFar(g);
moveCountLeft: Game -> nat
moveCountLeft(g) ==
MAX - moveCountSoFar(g);
movesForPlayer: Game * Player -> set of 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 = seq of Pos -- A legal game play sequence
inv moves ==
len moves = card elems 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 = seq1 of Player -- The order of play of the players
inv order ==
len order = card elems 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 not in set 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>
)
post if RESULT = <DRAW> then isDraw(game)
else if RESULT = <UNFINISHED> then isUnfinished(game)
else RESULT = whoWon(game);
end XO
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
