package at.ac.tuwien.dbai.alternation.examples;
/** Lexicographically First Maximal Clique **/
atm LFMC(UndirectedGraph<Integer> graph, UndirectedGraph.Node<Integer> vertex) {

UndirectedGraph.Node<Integer> node=vertex;

    state inClique {
        if (node.getObject().equals(1)){
            accept;
        }
        forall {
            for (int i=1;i<node.getObject();i++) {
                if(!graph.get(i).getNeighbours().contains(node)) {
                    notInClique{
                        node=graph.get(i);
                    }
                }
            }
        }
    }

    state notInClique {
        if (node.getObject().equals(1)){
            reject;
        }
        exists {
            for (int i=1;i<node.getObject();i++) {
                if(!graph.get(i).getNeighbours().contains(node)) {
                    inClique{
                        node=graph.get(i);
                    }
                }
            }
        }
    }
}