package de.bmoth.parser.ast.nodes.ltl;

public class BuechiAutomaton {

    public String new_name() {
        return "place holder";
    }
    
    public BuechiAutomatonNode[] expand(BuechiAutomatonNode node, BuechiAutomatonNode[] nodes_set) {
        return null;
    }

    public BuechiAutomatonNode[] create_graph(LTLFormula formula) {
        String[] initIncoming = {"init"};
        BuechiAutomatonNode[] nodes_set={};
        return expand(new BuechiAutomatonNode(new_name(), initIncoming, new LTLFormula[]{formula},
            new LTLFormula[]{}, new LTLFormula[]{}), nodes_set);
    }
}

@@ -137,133 +137,713 @@
   %7D%0A
+%0A
     
-%0A    public BuechiAutomatonNode%5B%5D expand(BuechiAutomatonNode node, BuechiAutomatonNode%5B%5D nodes_set) %7B%0A        return null
+public BuechiAutomatonNode nodeIsInNodeSet(BuechiAutomatonNode node, BuechiAutomatonNode%5B%5D nodesSet) %7B%0A        BuechiAutomatonNode foundNode = null;%0A        for (BuechiAutomatonNode nodeInSet: nodesSet) %7B%0A            if ((nodeInSet.processed == node.processed) && (nodeInSet.next == node.next)) %7B%0A                foundNode = nodeInSet;%0A                break;%0A            %7D%0A        %7D%0A        return foundNode;%0A    %7D%0A%0A    public BuechiAutomatonNode%5B%5D expand(BuechiAutomatonNode node, BuechiAutomatonNode%5B%5D nodesSet) %7B%0A        if (node.nonprocessed.length == 0) %7B%0A            if (nodeIsInNodeSet(node, nodesSet) != null) %7B%0A                return nodesSet;%0A            %7D%0A        %7D%0A        return nodesSet
 ;%0A  

Check if processed node is already in the nodesSet