+
+ /* Search through abstract repair actions & correspond data structure updates */
+ for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()!=TermNode.UPDATE)
+ continue;
+
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
+
+ cantremove.add(gn);
+ cantremove.add(gn2);
+
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn2)) {
+ if (!mustremove.contains(gn2)) {
+ change=true;
+ mustremove.add(gn2);
+ }
+ }
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
+ }
+ }
+
+ /* Searches individual conjunctions + abstract action +updates for cycles */
+ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ boolean foundnocycle=false;
+
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()!=TermNode.ABSTRACT)
+ continue;
+ AbstractRepair ar=tn2.getAbstract();
+ boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
+ int numadd=0;int numremove=0;
+
+ for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+ GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
+ GraphNode gn3=e2.getTarget();
+ TermNode tn3=(TermNode)gn3.getOwner();
+ if (tn3.getType()!=TermNode.UPDATE)
+ continue;
+
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
+ boolean containsgn3=cantremove.contains(gn3);
+ cantremove.add(gn);
+ cantremove.add(gn2);
+ cantremove.add(gn3);
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn3)) {
+ if (!mustremove.contains(gn3)) {
+ change=true;
+ mustremove.add(gn3);
+ }
+ }
+ if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
+ foundnocycle=true;
+ if (ismodify) {
+ MultUpdateNode mun=tn3.getUpdate();
+ if (mun.getType()==MultUpdateNode.ADD)
+ numadd++;
+ if (mun.getType()==MultUpdateNode.REMOVE)
+ numremove++;
+ }
+ }
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
+ if (!containsgn3)
+ cantremove.remove(gn3);
+ }
+ if (ismodify&&((numadd==0)||(numremove==0))) {
+ for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+ GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
+ GraphNode gn3=e2.getTarget();
+ TermNode tn3=(TermNode)gn3.getOwner();
+ if (tn3.getType()!=TermNode.UPDATE)
+ continue;
+ MultUpdateNode mun=tn3.getUpdate();
+ if (((mun.getType()==MultUpdateNode.ADD)||
+ (mun.getType()==MultUpdateNode.REMOVE))&&
+ (!mustremove.contains(gn3)))
+ mustremove.add(gn3);
+ }
+ }
+ }
+
+ if(!foundnocycle) {
+ if (!mustremove.contains(gn)) {
+ change=true;
+ mustremove.add(gn);
+ }
+ }
+ }
+
+ /* Searches scope nodes + compensation nodes */
+ for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ boolean foundcompensation=false;
+ if (nodes.contains(gn)) {
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+
+ if (tn2.getType()!=TermNode.UPDATE)
+ continue;
+ /* We have a compensation node */
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn2=cantremove.contains(gn2);
+ cantremove.add(gn);
+ cantremove.add(gn2);
+
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn2)) {
+ if (!mustremove.contains(gn2)) {
+ change=true;
+ mustremove.add(gn2);
+ }
+ } else {
+ if (!mustremove.contains(gn2))
+ foundcompensation=true;
+ }
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn2)
+ cantremove.remove(gn2);
+ }
+ }
+ if (!foundcompensation) {
+ for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()==TermNode.UPDATE) {
+ cantremove.add(gn2);
+ break;
+ }
+ }
+ }
+ }
+ couldremove.removeAll(mustremove);
+ couldremove.removeAll(cantremove);
+
+ Vector couldremovevector=new Vector();
+ couldremovevector.addAll(couldremove);
+ Vector combination=new Vector();
+ if(change)
+ continue; //recalculate
+
+ try {
+ GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
+ } catch (Exception e) {
+ e.printStackTrace();
+ System.exit(-1);
+ }
+
+ System.out.println("Searching set of "+couldremove.size()+" nodes.");
+ System.out.println("Eliminated must "+mustremove.size()+" nodes");
+ System.out.println("Eliminated cant "+cantremove.size()+" nodes");
+ System.out.println("Searching following set:");
+ for(Iterator it=couldremove.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ System.out.println(gn.getTextLabel());
+ }
+
+
+ while(true) {
+ if (illegal(combination,couldremovevector))
+ break;
+ Set combinationset=buildset(combination,couldremovevector);
+ checkmodify(combinationset);
+ combinationset.addAll(mustremove);
+ if (combinationset!=null) {
+ System.out.println("Checkabstract="+checkAbstract(combinationset));
+ System.out.println("Checkrepairs="+checkRepairs(combinationset));
+ System.out.println("Checkall="+checkAll(combinationset));
+
+ if (checkAbstract(combinationset)==0&&
+ checkRepairs(combinationset)==0&&
+ checkAll(combinationset)==0) {
+ return combinationset;
+ }
+ }
+ increment(combination,couldremovevector);
+ }
+ System.out.println("Search failed!");
+ return null;