Fixed some errors in the Repair Generator code.

[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 5b741c1e26a52a1aeae1b24c9e1e256e814cdbf4..d0197b5d8b000337659ead3f847cdd95b978cef4 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -277,11 +277,16 @@ public class Termination {
                TermNode tn2=(TermNode)gn2.getOwner();
                Conjunction conj=tn2.getConjunction();
                Constraint cons=tn2.getConstraint();
+               /* See if this is a relation wellformedness constraint
+                   that is trivially satisfied. */
+               System.out.println(gn.getTextLabel()+"---"+gn2.getTextLabel());
+               if (abstractinterferes.checkrelationconstraint(ar, cons))
+                   continue;
 
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (AbstractInterferes.interferes(ar,cons)||
-                       abstractinterferes.interferes(ar,dp)) {
+                   if (AbstractInterferes.interferesquantifier(ar,cons)||
+                       abstractinterferes.interfereswithpredicate(ar,dp)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        gn.addEdge(e);
                        break;
@@ -292,7 +297,7 @@ public class Termination {
                GraphNode gn2=(GraphNode)scopeiterator.next();
                TermNode tn2=(TermNode)gn2.getOwner();
                ScopeNode sn2=tn2.getScope();
-               if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+               if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
                    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                    gn.addEdge(e);
                }
@@ -345,8 +350,8 @@ public class Termination {
                Constraint constr=tn2.getConstraint();
                for(int i=0;i<conj.size();i++) {
                    DNFPredicate dp=conj.get(i);
-                   if (abstractinterferes.interferes(sn,dp)||
-                       AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
+                   if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
+                       AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
                        GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
                        GraphNode gnconseq=(GraphNode)consequence.get(sn);
                        gnconseq.addEdge(e);
@@ -358,13 +363,13 @@ public class Termination {
            /* Now see if this could effect other model defintion rules */
            for(int i=0;i<state.vRules.size();i++) {
                Rule r=(Rule) state.vRules.get(i);
-               if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
+               if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
                    GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
                    GraphNode gnconseq=(GraphNode)consequence.get(sn);
                    gnconseq.addEdge(e);
                }
-               if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
+               if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
                    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
                    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
                    GraphNode gnconseq=(GraphNode)consequence.get(sn);
@@ -542,7 +547,8 @@ public class Termination {
                generateremovefromsetrelation(gn,ar);
            } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
                /* Generate remove/add pairs */
-               generateremovefromsetrelation(gn,ar);
+               if (ar.needsRemoves(state))
+                   generateremovefromsetrelation(gn,ar);
                generateaddtosetrelation(gn,ar);
                /* Generate atomic modify */
                generatemodifyrelation(gn,ar);
@@ -938,7 +944,6 @@ public class Termination {
                }
            }
        }
-
     }
 
     boolean debugmsg(String st) {
@@ -1190,7 +1195,6 @@ public class Termination {
                } else {
                    return false;
                }
-               
            } else if (q instanceof SetQuantifier) {
                SetQuantifier sq=(SetQuantifier)q;
                if (un.getBinding(sq.var).getType()==Binding.SEARCH) {