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

cyclic atm CatAndMouse2(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;

    state mouseTurn {
        if (mousePosition==catPosition){
            reject;
        }
        exists{
            // mouse move
            for(Graph.Node child: mousePosition.getChildren()){
                catTurn{
                    mousePosition=child;
                }
            }

        }
    }

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