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

atm CatAndMouse(Graph<Integer> gameboard, Graph.Node<Integer> catStart, Graph.
                Node<Integer> mouseStart,Graph.Node<Integer> goal) {
    Graph.Node<Integer> catPosition=catStart;
    Graph.Node<Integer> mousePosition=mouseStart;
    int counter=0;

    state mouseTurn {
        if (mousePosition==catPosition){
            reject;
        }
        if (counter>gameboard.size()*gameboard.size()){
            reject;
        }
        exists{
            // mouse doesn't move
            catTurn{
                counter++;
            }
            // mouse move
            for(Graph.Node child: mousePosition.getChildren()){
                catTurn{
                    counter++;
                    mousePosition=child;
                }
            }
        }
    }

    state catTurn {
        if (mousePosition==goal){
            accept;
        }
        if (mousePosition==catPosition){
            reject;
        }
        forall{
            // cat doesn't move
            mouseTurn{
                counter++;
            }
            // cat move
            for(Graph.Node child: catPosition.getChildren()){
                if(child!=goal){
                    mouseTurn{
                        counter++;
                        catPosition=child;
                    }
                }
            }

        }
    }
}