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

public class BuechiAutomaton {

    public String new_name() {
        return "place holder";
    }

    public BuechiAutomatonNode nodeIsInNodeSet(BuechiAutomatonNode node, BuechiAutomatonNode[] nodesSet) {
        BuechiAutomatonNode foundNode = null;
        for (BuechiAutomatonNode nodeInSet: nodesSet) {
            if ((nodeInSet.processed == node.processed) && (nodeInSet.next == node.next)) {
                foundNode = nodeInSet;
                break;
            }
        }
        return foundNode;
    }

    public BuechiAutomatonNode[] expand(BuechiAutomatonNode node, BuechiAutomatonNode[] nodesSet) {
        if (node.nonprocessed.length == 0) {
            if (nodeIsInNodeSet(node, nodesSet) != null) {
                return nodesSet;
            }
        }
        return nodesSet;
    }

    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);
    }
}

@@ -33,16 +33,61 @@
 s.ltl;%0A%0A
+import org.apache.commons.lang3.ArrayUtils;%0A%0A
 public c
@@ -752,28 +752,56 @@
             
-if (
+BuechiAutomatonNode nodeInSet = 
 nodeIsInNode
@@ -819,16 +819,43 @@
 odesSet)
+;%0A            if (nodeInSet
  != null
@@ -870,39 +870,320 @@
             
-return nodesSet
+node.incoming = ArrayUtils.addAll(node.incoming, nodeInSet.incoming);%0A                return nodesSet;%0A            %7D else %7B%0A                return expand(new BuechiAutomatonNode(new_name(), new String%5B%5D%7Bnode.name%7D, node.next,%0A                    new LTLFormula%5B%5D%7B%7D, new LTLFormula%5B%5D%7B%7D), nodesSet)
 ;%0A          

Handle both cases of a finished node