% This specification describes the game `Clobber', which is a two
% player board game. There is a board of 8 by 8 (although below
% we describe a board of 4 by 4, as otherwise the state space is
% prohibitively big). One player has white pieces  (0) and the
% other has black pieces (X). Initially, the board is set up as:
%
%      0 X 0 X 0 X 0 X
%      X 0 X 0 X 0 X 0
%      0 X 0 X 0 X 0 X
%      X 0 X 0 X 0 X 0
%      0 X 0 X 0 X 0 X
%      X 0 X 0 X 0 X 0
%      0 X 0 X 0 X 0 X
%      X 0 X 0 X 0 X 0
%
% Black makes the first move and players alternatingly make a move. A
% player makes a turn by moving a piece
% of its own color horizontally or vertically to a position with a
% piece of the opposite color and it removes that piece. This is
% the only move that is allowed. The first player that cannot do a
% move looses the game.
%
% Thanks go to Mark Winands for explaining the game.
%
% Reijkjavik, May 9, 2006, Jan Friso Groote

sort Position = struct Black | White | Empty;
sort Direction = struct Up | Right | Down | Left;
map N,M:Pos;
eqn N=4;
    M=4;

sort Row=List(Position);
     Board=List(Row);
map  At:Pos#Pos#Board->Position;
     At:Pos#Pos#Direction#Board->Position;
     At:Pos#Row->Position;
     Put:Position#Pos#Pos#Board->Board;
     Put:Position#Pos#Pos#Direction#Board->Board;
     Put:Position#Pos#Row->Row;
     CanMove:Pos#Pos#Position#Position#Board->Bool;

var b:Board;
    r:Row;
    p,p':Position;
    x,y:Pos;
eqn At(x,y,Up,b)=At(x,y+1,b);
    At(x,y,Right,b)=At(x+1,y,b);
    y>1 -> At(x,y,Down,b)=At(x,Int2Pos(y-1),b);
    y==1 -> At(x,y,Down,b)=Empty;
    x>1 -> At(x,y,Left,b)=At(Int2Pos(x-1),y,b);
    x==1 -> At(x,y,Left,b)=Empty;
    At(x,y,[])=Empty;
    y==1 -> At(x,y,r|>b)=At(x,r);
    y>M -> At(x,y,b)=Empty;
    1<y && y<=M -> At(x,y,r|>b)=At(x,Int2Pos(y-1),b);
    At(x,[])=Empty;
    x==1 -> At(x,p|>r)=p;
    x>N -> At(x,p|>r)=Empty;
    1<x && x<=N -> At(x,p|>r)=At(Int2Pos(x-1),r);
    Put(p,x,y,Up,b)=Put(p,x,y+1,b);
    Put(p,x,y,Right,b)=Put(p,x+1,y,b);
    y>1 -> Put(p,x,y,Down,b)=Put(p,x,Int2Pos(y-1),b);
    x>1 -> Put(p,x,y,Left,b)=Put(p,Int2Pos(x-1),y,b);
    y==1 -> Put(p,x,y,r|>b)=Put(p,x,r)|>b;
    y>1 -> Put(p,x,y,r|>b)=r|>Put(p,x,Int2Pos(y-1),b);
    x==1 -> Put(p,x,p'|>r)=p|>r;
    x>1 -> Put(p,x,p'|>r)=p'|>Put(p,Int2Pos(x-1),r);

    x==N && y==M ->
      CanMove(x,y,p,p',b)=
         At(x,y,b)==p &&
            ( At(x,y,Down,b)==p' || At(x,y,Left,b)==p');

    x==N && y<M ->
      CanMove(x,y,p,p',b)=
         (At(x,y,b)==p &&
            (At(x,y,Up,b)==p' ||
             At(x,y,Down,b)==p' || At(x,y,Left,b)==p')) ||
          CanMove(1,y+1,p,p',b);

    x<N ->
      CanMove(x,y,p,p',b)=
         (At(x,y,b)==p &&
            (At(x,y,Up,b)==p' || At(x,y,Right,b)==p' ||
             At(x,y,Down,b)==p' || At(x,y,Left,b)==p')) ||
          CanMove(x+1,y,p,p',b);


act WhiteMove,BlackMove:Pos#Pos#Direction;
    WhiteWins,BlackWins;

proc Clobber(b:Board,WhiteMoves:Bool)=
       sum x,y:Pos, dir:Direction.
                    (WhiteMoves &&
                     x<=N && y<=M &&
                     At(x,y,b)==White &&
                     At(x,y,dir,b)==Black)->
           WhiteMove(x,y,dir).
             Clobber(Put(White,x,y,dir,Put(Empty,x,y,b)),false)+
       sum x,y:Pos, dir:Direction.
                    (!WhiteMoves &&
                     x<=N && y<= M &&
                     At(x,y,b)==Black &&
                     At(x,y,dir,b)==White)->
           BlackMove(x,y,dir).
             Clobber(Put(Black,x,y,dir,Put(Empty,x,y,b)),true)+
       (WhiteMoves && !CanMove(1,1,White,Black,b)) ->
             BlackWins.Clobber(b,WhiteMoves)+
       (!WhiteMoves && !CanMove(1,1,Black,White,b)) ->
             WhiteWins.Clobber(b,WhiteMoves)+
       delta;


init Clobber([[Black,White,Black,White],
              [White,Black,White,Black],
              [Black,White,Black,White],
              [White,Black,White,Black]],false);
