% This mCRL2 specification describes the game 'four in a row'.
% Four in a row is a two player game that alternatingly put a
% yellow and red piece on the lowest non occupied position of
% the board. Red starts the game. The player who puts a piece 
% first such that there
% are four pieces in a row on the board in either horizontal,
% vertical or diagonal direction wins the game. The standard
% game has 5 rows and seven columns. A typical situation where
% red wins the game is the following:
%
%        . . . . . . .
%        . . . . . . .
%        . . . R . . .
%        . . R R . . .        R is red
%        . R R Y . . .        Y is yellow
%        R Y Y Y . . Y
%
% To generate the state space of this game, the following
% sequence of commands can be used. Using lpsparunfold and
% lpsconstelm the structure of the board is eliminated in
% favour of single variables, which speeds up the generation
% of the state space dramatically. The size of the state space
% is much larger than 2 10^9 states. Generation of the complete
% state space is technically not yet possible.
%
% mcrl22lps -vD four_in_a_row.mcrl2 temp.lps &&
% lpssuminst -v temp.lps | lpsparunfold -l -sBoard -v -n5 | lpsparunfold -l -sRow -v -n7 | lpsrewr -v > temp1.lps &&
% lpsconstelm -v -c -rjittyc temp1.lps temp2.lps &&
% lps2lts -v -rjittyc temp2.lps 
%
% Using the following formula, it can be determined whether red has 
% winning strategy.
%
%    mu X.(exists x:Pos.<RedMoves(x)>
%            (<RedWins>true || 
%             ((exists y:Pos.<YellowMoves(y)>true) && forall y:Pos.[YellowMoves(y)](X && [YellowWins]false))))
%
% Using pbes2bool this formula can be verified on smaller than the full board.
% The table below shows on which boards red has a winning strategy.
% This has been verified using pbes2bool -rjittyc -v -s2 -zd temp1.pbes --erase=some
% For 7x4 and 5x6 boards typically 40Gbyte memory was required.
%
%       Columns
% Rows    1     2     3     4     5     6     7
%   1     No    No    No    No    No    No    No  
%   2     No    No    No    No    No    No    No
%   3     No    No    No    No    No    No    No
%   4     No    No    No    No    No    No    No
%   5     No    No    No    No    No    No
%   6     No    No    No    No    No
%
% Jan Friso Groote, April 6, 2010/Juli 28, 2014

sort Piece = struct Red | Yellow | None;
map N,M,R:Pos;
eqn N=7;     %Number of columns (default 7)
    M=6;     %Number of rows (default 6)
    R=4;     %Length of a winning sequence of the same color (default 4)

sort Row=List(Piece);
     Board=List(Row);

map  At:Nat#Nat#Board->Piece;                       % At(x,y,b) give the piece at position x,y. If there is no
                                                    % piece, or if x,y is outside the board, give None.
     At:Nat#Row->Piece;                             % See At above. Now for a single row.
     PutColumn:Piece#Pos#Board->Board;              % Put piece p at the indicated column in a board, assuming
                                                    % that there is a free spot.
     PutColumn:Piece#Pos#Pos#Board->Board;          % Put piece at the indicated column in a board, assuming that
                                                    % there is a free spot and the second argument of type Pos
                                                    % indicates the lowest position to try first.
     Put:Piece#Pos#Pos#Board->Board;                % Put piece at the indicated position on the board.
     Put:Piece#Pos#Row->Row;                        % Put piece p at the indicated position in a row.

     Four_in_a_row:Piece#Board->Bool;               % Indicates whether there are four pieces of sort Piece 
                                                    % either horizontally, vertically or diagonally in a row.
     Four_in_a_row_horizontally:Piece#Board->Bool;               
     Four_in_a_row_horizontally:Piece#Pos#Board->Bool; % Check from the indicated row upwards.
     Count_rows_horizontally:Piece#Pos#Pos#Board#Nat->Bool; % Count the number of pieces in a row, and return
                                                            % true when four in a row have been found.
     Four_in_a_row_vertically:Piece#Board->Bool;               
     Four_in_a_row_vertically:Piece#Pos#Board->Bool; % Check from the indicated row upwards.
     Count_rows_vertically:Piece#Pos#Pos#Board#Nat->Bool; 

     Four_in_a_row_diagonally:Piece#Board->Bool;               
     Four_in_a_row_diagonally_column:Piece#Pos#Board->Bool; % Check from the first column diagonally.
     Four_in_a_row_diagonally_row:Piece#Pos#Board->Bool; % Check from the first row diagonally.
     Count_rows_diagonally:Piece#Pos#Pos#Board#Nat->Bool; 
     Count_rows_diagonally':Piece#Pos#Pos#Board#Nat->Bool; 

var  b,b':Board;
     r:Row;
     p,p',p'':Piece;
     x,y:Nat;
     c:Bool;
     z:Pos;

eqn  if(c,true,false)=c;
     if(c,false,true)=!c;
     if(c,p,p')==p'' = if(c,p==p'',p'==p'');
     y==1 -> At(x,y,r|>b)=At(x,r);
     1<y && y<=M -> At(x,y,r|>b)=At(x,Int2Nat(y-1),b);
     y==0 || y>M || x==0 || x>N -> At(x,y,b)=None;
     At(x,y,if(c,b,b'))=if(c,At(x,y,b),At(x,y,b'));  % This rewrite rule is instrumental to let lpsconstelm 
                                                     % reduce the system substantially, after applying lpsparunfold.
     x==1 -> At(x,p|>r)=p;
     1<x && x<=N -> At(x,p|>r)=At(Int2Nat(x-1),r);
     x==0 || x>N -> At(x,p|>r)=None;
     At(x,Put(p,z,r))=if(x==z,p,At(x,r));

var  b,b':Board;
     r:Row;
     p,p':Piece;
     x,y:Pos;
     dx,dy:Int;
     c,othercolorseen:Bool;
     count:Nat;
eqn  y==1 -> Put(p,x,y,r|>b)=Put(p,x,r)|>b;
     y>1 && y<=M -> Put(p,x,y,r|>b)=r|>Put(p,x,Int2Pos(y-1),b);
     Put(p,x,y,if(c,b,b'))=if(c,Put(p,x,y,b),Put(p,x,y,b'));  % See comments for distribution of At over if.
     x==1 -> Put(p,x,p'|>r)=p|>r;
     x>1 && x<=N -> Put(p,x,p'|>r)=p'|>Put(p,Int2Pos(x-1),r);
 
     PutColumn(p,x,b)=PutColumn(p,x,1,b);
     y<M -> PutColumn(p,x,y,b)=if(At(x,y,b)==None,Put(p,x,y,b),PutColumn(p,x,y+1,b));
     y==M -> PutColumn(p,x,y,b)=Put(p,x,M,b);
 
     Four_in_a_row(p,b)=
            Four_in_a_row_horizontally(p,b)||
            Four_in_a_row_vertically(p,b)||
            Four_in_a_row_diagonally(p,b);
 
     Four_in_a_row_horizontally(p,b)=Four_in_a_row_horizontally(p,1,b);
     y<M -> Four_in_a_row_horizontally(p,y,b)=Count_rows_horizontally(p,1,y,b,0) ||
                                              Four_in_a_row_horizontally(p,y+1,b);
     y==M -> Four_in_a_row_horizontally(p,y,b)=Count_rows_horizontally(p,1,M,b,0);
     x<N -> Count_rows_horizontally(p,x,y,b,count)=
                                       if(At(x,y,b)==p,
                                         count>=R-1 || Count_rows_horizontally(p,x+1,y,b,count+1),
                                         Count_rows_horizontally(p,x+1,y,b,0));
     x==N -> Count_rows_horizontally(p,x,y,b,count)=if(At(N,y,b)==p,count>=R-1,false);
 
     Four_in_a_row_vertically(p,b)=Four_in_a_row_vertically(p,1,b);
     x<N -> Four_in_a_row_vertically(p,x,b)=Count_rows_vertically(p,x,1,b,0) ||
                                              Four_in_a_row_vertically(p,x+1,b);
     x==N -> Four_in_a_row_vertically(p,x,b)=Count_rows_vertically(p,N,1,b,0);
     y<M ->  Count_rows_vertically(p,x,y,b,count)=
                                       if(At(x,y,b)==p,
                                         count>=R-1 || Count_rows_vertically(p,x,y+1,b,count+1),
                                         Count_rows_vertically(p,x,y+1,b,0));
     y==M -> Count_rows_vertically(p,x,y,b,count)=if(At(x,M,b)==p,count>=R-1,false);
 
     Four_in_a_row_diagonally(p,b)=Four_in_a_row_diagonally_column(p,2,b) || 
                                   Four_in_a_row_diagonally_row(p,1,b);
     x<N -> Four_in_a_row_diagonally_row(p,x,b)=Count_rows_diagonally(p,x,1,b,0) ||
                                                Count_rows_diagonally'(p,x,1,b,0) ||
                                                Four_in_a_row_diagonally_row(p,x+1,b);
     x==N -> Four_in_a_row_diagonally_row(p,x,b)=Count_rows_diagonally'(p,N,1,b,0);
     y<M -> Four_in_a_row_diagonally_column(p,y,b)=Count_rows_diagonally(p,1,y,b,0) ||
                                                   Count_rows_diagonally'(p,N,y,b,0) ||
                                                   Four_in_a_row_diagonally_column(p,y+1,b);
     y>=M -> Four_in_a_row_diagonally_column(p,y,b)=false;
     x<N && y<M ->  Count_rows_diagonally(p,x,y,b,count)=
                                       if(At(x,y,b)==p,
                                         count>=R-1 || Count_rows_diagonally(p,x+1,y+1,b,count+1),
                                         Count_rows_diagonally(p,x+1,y+1,b,0));
     x==N || y==M -> Count_rows_diagonally(p,x,y,b,count)=if(At(x,y,b)==p,count>=R-1,false);
     x>1 && y<M ->  Count_rows_diagonally'(p,x,y,b,count)=
                                       if(At(x,y,b)==p,
                                         count>=R-1 || Count_rows_diagonally'(p,max(1,x-1),y+1,b,count+1),
                                         Count_rows_diagonally'(p,max(1,x-1),y+1,b,0));
     x==1 || y==M -> Count_rows_diagonally'(p,x,y,b,count)=if(At(x,y,b)==p,count>=R-1,false);


act  YellowMoves,RedMoves:Pos;
     YellowWins,RedWins;
proc FourInaRow(b:Board,WhoMoves:Piece)=
       sum x:Pos.(WhoMoves==Yellow && 
                  x<=N &&
                  At(x,M,b)==None) ->
             YellowMoves(x).
                FourInaRow(PutColumn(Yellow,x,b),Red)+

       sum x:Pos.(WhoMoves==Red && 
                  x<=N &&
                  At(x,M,b)==None) ->
             RedMoves(x).
                FourInaRow(PutColumn(Red,x,b),Yellow)+

       (WhoMoves==Yellow && Four_in_a_row(Red,b)) ->
             RedWins.
                FourInaRow(b,None)+

       (WhoMoves==Red && Four_in_a_row(Yellow,b)) ->
             YellowWins.
                FourInaRow(b,None);
                  
% Note that the board is reversed. The bottom row is drawn at the top.
map initial_board:Board;
eqn initial_board= [[None,  None,  None,  None,  None,  None,  None  ],
                    [None,  None,  None,  None,  None,  None,  None  ],
                    [None,  None,  None,  None,  None,  None,  None  ],
                    [None,  None,  None,  None,  None,  None,  None  ],
                    [None,  None,  None,  None,  None,  None,  None  ],
                    [None,  None,  None,  None,  None,  None,  None  ]];


init FourInaRow(initial_board,Red);
