Added support to printout data structure update nodes (bindings/updates)

[repair.git] / Repair / RepairCompiler / MCC / IR / Termination.java

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 271d9f2fca7744ba18f945b9e12ef036da4e58bb..f3d134fa2e44fc4baea1b5c75f5b817127868707 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -47,17 +47,24 @@ public class Termination {
 
        HashSet superset=new HashSet();
        superset.addAll(conjunctions);
-       superset.addAll(abstractrepair);
+       //superset.addAll(abstractrepair);
        //superset.addAll(updatenodes);
        //superset.addAll(scopenodes);
        //superset.addAll(consequencenodes);
-       //GraphNode.computeclosure(superset);
+       GraphNode.computeclosure(superset);
        try {
            GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
        } catch (Exception e) {
            e.printStackTrace();
            System.exit(-1);
        }
+       for(Iterator it=updatenodes.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode)it.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           MultUpdateNode mun=tn.getUpdate();
+           System.out.println(gn.getTextLabel());
+           System.out.println(mun.toString());
+       }
     }
     
     void generateconjunctionnodes() {
@@ -180,7 +187,7 @@ public class Termination {
                for(int j=0;j<array.length;j++) {
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d);
                    TermNode tn2=new TermNode(ar);
-                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
                    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
                    gn.addEdge(e);
                    abstractrepair.add(gn2);
@@ -294,7 +301,9 @@ public class Termination {
                        continue;
                    }
                }
-
+               if (!un.checkupdates()) /* Make sure we have a good update */
+                   continue;
+               
                mun.addUpdate(un);
 
                GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
@@ -392,6 +401,10 @@ public class Termination {
                        goodflag=false;break;
                    }
                }
+               if (!un.checkupdates()) {
+                   goodflag=false;
+                   break;
+               }
                mun.addUpdate(un);
            }
            if (goodflag) {
@@ -593,7 +606,8 @@ public class Termination {
                    GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 
                    if (processquantifers(gn2,un, r)&&debugdd()&&
-                       processconjunction(un,ruleconj)) {
+                       processconjunction(un,ruleconj)&&
+                       un.checkupdates()) {
                        //System.out.println("Attempting to generate add to set #5");
                        mun.addUpdate(un);
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);