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

simple atm CatAndMouse3(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 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;
                    }
                }
            }

        }
    }
}