package at.ac.tuwien.dbai.alternation.examples;

atm TicTacToe (byte[] game, boolean crossPlayersTurn) {
    byte[] paper = game.clone();

    state start {
        if (crossPlayersTurn){
            forall{
                crossPlayer{
                }
            }
        } else {
            forall{
                noughtPlayer{
                }
            }
        }
    }

    state crossPlayer {
        // check if there are three noughts in a row
        if(paper[4]==2){
            if ( paper[0]==2 & paper[8]==2) reject;
            if ( paper[1]==2 & paper[7]==2) reject;
            if ( paper[2]==2 & paper[6]==2) reject;
            if ( paper[3]==2 & paper[5]==2) reject;
        }
        if (paper[0]==2 & paper[1]==2 & paper[2]==2) reject;
        if (paper[0]==2 & paper[3]==2 & paper[6]==2) reject;
        if (paper[2]==2 & paper[5]==2 & paper[8]==2) reject;
        if (paper[6]==2 & paper[7]==2 & paper[8]==2) reject;

        exists{
            for (int i=0;i<9;i++){
                if (paper[i]==0){
                    noughtPlayer{
                        paper[i]=1;
                    }
                }
            }
        }
    }

    state noughtPlayer{
        // check if there are three crosses in a row
        if(paper[4]==1){
            if ( paper[0]==1 & paper[8]==1) accept;
            if ( paper[1]==1 & paper[7]==1) accept;
            if ( paper[2]==1 & paper[6]==1) accept;
            if ( paper[3]==1 & paper[5]==1) accept;
        }
        if (paper[0]==1 & paper[1]==1 & paper[2]==1) accept;
        if (paper[0]==1 & paper[3]==1 & paper[6]==1) accept;
        if (paper[2]==1 & paper[5]==1 & paper[8]==1) accept;
        if (paper[6]==1 & paper[7]==1 & paper[8]==1) accept;

        if(paper[0]!=0 & paper[1]!=0 & paper[2]!=0 & paper[3]!=0 & paper[4]!=0 &
           paper[5]!=0 & paper[6]!=0 & paper[7]!=0 & paper[8]!=0){
            reject;
        }
        forall {
            for (int i=0;i<9;i++){
                if (paper[i]==0){
                    crossPlayer{
                        paper[i]=2;
                    }
                }
            }
        }
    }
}