Updates
authorbdemsky <bdemsky>
Thu, 18 Dec 2003 19:23:26 +0000 (19:23 +0000)
committerbdemsky <bdemsky>
Thu, 18 Dec 2003 19:23:26 +0000 (19:23 +0000)
21 files changed:
Repair/RepairCompiler/MCC/IR/ComparisonPredicate.java
Repair/RepairCompiler/MCC/IR/Conjunction.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/Constraint.java
Repair/RepairCompiler/MCC/IR/DNFConstraint.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/DNFExpr.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/DNFPredicate.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/DNFRule.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/DependencyBuilder.java
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ExprPredicate.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
Repair/RepairCompiler/MCC/IR/LogicStatement.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/Optimizer.java
Repair/RepairCompiler/MCC/IR/Predicate.java
Repair/RepairCompiler/MCC/IR/RuleConjunction.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/SemanticChecker.java
Repair/RepairCompiler/MCC/IR/SetAnalysis.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/SizeofPredicate.java
Repair/RepairCompiler/MCC/IR/Termination.java [new file with mode: 0755]

index 54b64ad..63390e9 100755 (executable)
@@ -34,6 +34,10 @@ public class ComparisonPredicate extends Predicate {
         return v;
     }
 
+    public int[] getRepairs(boolean negated) {
+       return new int[] {AbstractRepair.MODIFYRELATION};
+    }
+
     public void generate(CodeWriter writer, VarDescriptor vd) {
         // get (first) value for quantifer.relation ... then do comparison with expr... 
         // can this be maybe? i guess if quantifer.relation is empty
diff --git a/Repair/RepairCompiler/MCC/IR/Conjunction.java b/Repair/RepairCompiler/MCC/IR/Conjunction.java
new file mode 100755 (executable)
index 0000000..82e115f
--- /dev/null
@@ -0,0 +1,43 @@
+package MCC.IR;
+import java.util.*;
+
+public class Conjunction {
+
+    Vector predicates;
+    public Conjunction(DNFPredicate pred) {
+       predicates=new Vector();
+       predicates.add(pred);
+    }
+    Conjunction(Vector preds){
+       predicates=preds       ;
+    }
+
+    int size() {
+       return predicates.size();
+    }
+    
+    DNFPredicate get(int i) {
+       return (DNFPredicate) predicates.get(i);
+    }
+
+    void add(DNFPredicate dp) {
+       predicates.add(dp);
+    }
+
+    public Conjunction append(Conjunction c) {
+       Conjunction copy=copy();
+       for(int i=0;i<c.size();i++) {
+           copy.add(new DNFPredicate(c.get(i)));
+       }
+       return copy;
+    }
+
+    public Conjunction copy() {
+       Vector vector=new Vector();
+       for (int i=0;i<size();i++) {
+           DNFPredicate dp=get(i);
+           vector.add(new DNFPredicate(dp));
+       }
+       return new Conjunction(vector);
+    }
+}
index 852313a..97a2c24 100755 (executable)
@@ -11,7 +11,7 @@ public class Constraint {
     SymbolTable st = new SymbolTable();
     Vector quantifiers = new Vector(); 
     LogicStatement logicstatement = null;
-
+    DNFConstraint dnfconstraint;
     int num;
 
     public Constraint() {
@@ -37,6 +37,8 @@ public class Constraint {
 
     public void setLogicStatement(LogicStatement ls) {
         logicstatement = ls;
+       // Construct DNF form for analysis
+       dnfconstraint=logicstatement.constructDNF();
     }
 
     public LogicStatement getLogicStatement() {
diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
new file mode 100755 (executable)
index 0000000..1f3849f
--- /dev/null
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+
+public class DNFConstraint {
+   Vector conjunctions;
+
+    public DNFConstraint(Predicate p) {
+       conjunctions=new Vector();
+       conjunctions.add(new Conjunction(new DNFPredicate(true,p)));
+    }
+
+    public DNFConstraint(Conjunction conj) {
+       conjunctions=new Vector();
+       conjunctions.add(conj);
+    }
+
+    public DNFConstraint(Vector conj) {
+       conjunctions=conj;
+    }
+    
+    DNFConstraint() {
+       conjunctions=new Vector();
+    }
+
+    int size() {
+       return conjunctions.size();
+    }
+
+    Conjunction get(int i) {
+       return (Conjunction)conjunctions.get(i);
+    }
+
+    void add(Conjunction c) {
+       conjunctions.add(c);
+    }
+
+    public DNFConstraint copy() {
+       Vector vector=new Vector();
+       for (int i=0;i<size();i++) {
+           vector.add(get(i).copy());
+       }
+       return new DNFConstraint(vector);
+    }
+
+    public DNFConstraint and(DNFConstraint c) {
+       DNFConstraint newdnf=new DNFConstraint();
+       for(int i=0;i<size();i++) {
+           for(int j=0;j<c.size();j++) {
+               newdnf.add(get(i).append(c.get(j))); //Cross product
+           }
+       }
+       return newdnf;
+    }
+
+    public DNFConstraint or(DNFConstraint c) {
+       DNFConstraint copy=copy();
+       for(int i=0;i<c.size();i++) {
+           copy.add(c.get(i).copy()); //Add in other conjunctions
+       }
+       return copy;
+    }
+
+    public DNFConstraint not() {
+       DNFConstraint copy=copy();
+       for (int i=0;i<size();i++) {
+           Conjunction conj=get(i);
+           for (int j=0;j<conj.size();j++) {
+               DNFPredicate dp=conj.get(j);
+               dp.negatePred();
+           }
+       }
+       return copy;
+   }
+}
+
+
diff --git a/Repair/RepairCompiler/MCC/IR/DNFExpr.java b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
new file mode 100755 (executable)
index 0000000..ce039db
--- /dev/null
@@ -0,0 +1,19 @@
+package MCC.IR;
+
+public class DNFExpr {
+    boolean negate;
+    Expr predicate;
+
+    public DNFExpr(DNFExpr dp) {
+       this.negate=dp.negate;
+       this.predicate=dp.predicate;
+    }
+
+    public DNFExpr(boolean negate,Expr predicate) {
+       this.negate=negate;
+       this.predicate=predicate;
+    }
+    void negatePred() {
+       negate=!negate;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/DNFPredicate.java b/Repair/RepairCompiler/MCC/IR/DNFPredicate.java
new file mode 100755 (executable)
index 0000000..2328bfc
--- /dev/null
@@ -0,0 +1,21 @@
+package MCC.IR;
+
+public class DNFPredicate {
+    boolean negate;
+    Predicate predicate;
+
+    public DNFPredicate(DNFPredicate dp) {
+       this.negate=dp.negate;
+       this.predicate=dp.predicate;
+    }
+    Predicate getPredicate() {
+       return predicate;
+    }
+    public DNFPredicate(boolean negate,Predicate predicate) {
+       this.negate=negate;
+       this.predicate=predicate;
+    }
+    void negatePred() {
+       negate=!negate;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
new file mode 100755 (executable)
index 0000000..942f7f6
--- /dev/null
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+
+public class DNFRule {
+   Vector ruleconjunctions;
+
+    public DNFRule(Expr e) {
+       ruleconjunctions=new Vector();
+       ruleconjunctions.add(new RuleConjunction(new DNFExpr(true,e)));
+    }
+
+    public DNFRule(RuleConjunction conj) {
+       ruleconjunctions=new Vector();
+       ruleconjunctions.add(conj);
+    }
+
+    public DNFRule(Vector conj) {
+       ruleconjunctions=conj;
+    }
+    
+    DNFRule() {
+       ruleconjunctions=new Vector();
+    }
+
+    int size() {
+       return ruleconjunctions.size();
+    }
+
+    RuleConjunction get(int i) {
+       return (RuleConjunction)ruleconjunctions.get(i);
+    }
+
+    void add(RuleConjunction c) {
+       ruleconjunctions.add(c);
+    }
+
+    public DNFRule copy() {
+       Vector vector=new Vector();
+       for (int i=0;i<size();i++) {
+           vector.add(get(i).copy());
+       }
+       return new DNFRule(vector);
+    }
+
+    public DNFRule and(DNFRule c) {
+       DNFRule newdnf=new DNFRule();
+       for(int i=0;i<size();i++) {
+           for(int j=0;j<c.size();j++) {
+               newdnf.add(get(i).append(c.get(j))); //Cross product
+           }
+       }
+       return newdnf;
+    }
+
+    public DNFRule or(DNFRule c) {
+       DNFRule copy=copy();
+       for(int i=0;i<c.size();i++) {
+           copy.add(c.get(i).copy()); //Add in other conjunctions
+       }
+       return copy;
+    }
+
+    public DNFRule not() {
+       DNFRule copy=copy();
+       for (int i=0;i<size();i++) {
+           RuleConjunction conj=get(i);
+           for (int j=0;j<conj.size();j++) {
+               DNFExpr dp=conj.get(j);
+               dp.negatePred();
+           }
+       }
+       return copy;
+   }
+}
+
+
index babdd0e..c913a26 100755 (executable)
@@ -79,7 +79,7 @@ public class DependencyBuilder {
                         otherrulenode.addEdge(new GraphNode.Edge(d.getSymbol(), rulenode));
                     }
                 }
-            }           
+            }
         }
 
         /* build constraint->rule dependencies */
index 1e7fd14..cd82227 100755 (executable)
@@ -25,4 +25,8 @@ public abstract class Expr {
         throw new IRException("unsupported");
     }
 
+    public DNFRule constructDNF() {
+       return new DNFRule(this);
+    }
+
 }
index 4508867..3242de1 100755 (executable)
@@ -25,6 +25,9 @@ public class ExprPredicate extends Predicate {
     public void generate(CodeWriter writer, VarDescriptor dest) {
         expr.generate(writer, dest);
     }
-            
+
+    public int[] getRepairs(boolean negated) {
+       return new int[] {};
+    }
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java b/Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
new file mode 100755 (executable)
index 0000000..adea1ff
--- /dev/null
@@ -0,0 +1,119 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+public class ImplicitSchema {
+    State state;
+    SetAnalysis setanalysis;
+    public ImplicitSchema(State state) {
+       this.state=state;
+       this.setanalysis=new SetAnalysis(state);
+    }
+
+    public void update() {
+       updaterules();
+       updateconstraints();
+       updaterelationconstraints();
+    }
+
+    void updaterelationconstraints() {
+       Vector reldescriptors=state.stRelations.getAllDescriptors();
+       for(int i=0;i<reldescriptors.size();i++) {
+           RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
+           Constraint c=new Constraint();
+           
+           /* Construct quantifier */
+           RelationQuantifier rq=new RelationQuantifier();
+           String varname1=new String("partitionvar1");
+           String varname2=new String("partitionvar2");
+           VarDescriptor var1=new VarDescriptor(varname1);
+           VarDescriptor var2=new VarDescriptor(varname2);
+           c.getSymbolTable().add(var1);
+           c.getSymbolTable().add(var2);
+           var1.setType(rd.getDomain().getType());
+           var2.setType(rd.getRange().getType());
+           rq.setTuple(var1,var2);
+           rq.setRelation(rd);
+           c.addQuantifier(rq);
+
+           VarExpr ve1=new VarExpr(varname1);
+           SetExpr se1=new SetExpr(rd.getDomain());
+           LogicStatement incpred1=new InclusionPredicate(ve1,se1);
+
+           VarExpr ve2=new VarExpr(varname2);
+           SetExpr se2=new SetExpr(rd.getRange());
+           LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+           c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
+           state.vConstraints.add(c);
+       }
+    }
+
+    void updateconstraints() {
+       Vector setdescriptors=state.stSets.getAllDescriptors();
+       for(int i=0;i<setdescriptors.size();i++) {
+           SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
+           if(sd.isPartition()) {
+               Constraint c=new Constraint();
+
+               /* Construct quantifier */
+               SetQuantifier sq=new SetQuantifier();
+               String varname=new String("partitionvar");
+               VarDescriptor var=new VarDescriptor(varname);
+               c.getSymbolTable().add(var);
+               var.setType(sd.getType());
+               sq.setVar(var);
+               sq.setSet(sd);
+               c.addQuantifier(sq);
+
+               /*Construct logic statement*/
+               LogicStatement ls=null;
+               for(int j=0;j<sd.getSubsets().size();j++) {
+                   LogicStatement conj=null;
+                   for(int k=0;k<sd.getSubsets().size();k++) {
+                       VarExpr ve=new VarExpr(varname);
+                       SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+                       LogicStatement incpred=new InclusionPredicate(ve,se);
+                       if (j!=k) {
+                           incpred=new LogicStatement(LogicStatement.NOT ,incpred);
+                       }
+                       if (conj==null)
+                           conj=incpred;
+                       else 
+                           conj=new LogicStatement(LogicStatement.AND, conj, incpred);
+                   }
+                   if (ls==null)
+                       ls=conj;
+                   else 
+                       ls=new LogicStatement(LogicStatement.OR, ls, conj);
+               }
+               c.setLogicStatement(ls);
+               state.vConstraints.add(c);
+           }
+       }
+    }
+    
+    void updaterules() {
+       Vector oldrules=state.vRules;
+       Vector newrules=new Vector();
+       for(int i=0;i<oldrules.size();i++) {
+           Rule r=(Rule)oldrules.get(i);
+           if (r.inclusion instanceof SetInclusion) {
+               SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
+               Set supersets=setanalysis.getSuperset(sd);
+               if (supersets!=null)
+                   for(Iterator superit=supersets.iterator();superit.hasNext();) {
+                       SetDescriptor sd1=(SetDescriptor)superit.next();
+                       Rule nr=new Rule();
+                       nr.guard=r.guard;
+                       nr.quantifiers=r.quantifiers;
+                       nr.isstatic=r.isstatic;
+                       nr.isdelay=r.isdelay;
+                       nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
+                       nr.st=r.st;
+                       newrules.add(nr);
+                   }
+           }
+       }
+       oldrules.addAll(newrules);
+    }
+}
index fd4d8ff..26b9f4a 100755 (executable)
@@ -40,6 +40,19 @@ public class InclusionPredicate extends Predicate {
         //set.addAll(expr.getInversedRelations());
         //return set;
     }
-            
+
+    public int[] getRepairs(boolean negated) {
+       if (setexpr instanceof ImageSetExpr) {
+           if (negated)
+               return new int[] {AbstractRepair.REMOVEFROMRELATION};
+           else
+               return new int[] {AbstractRepair.ADDTORELATION};
+       } else {
+           if (negated)
+               return new int[] {AbstractRepair.REMOVEFROMSET};
+           else
+               return new int[] {AbstractRepair.ADDTOSET};
+       }
+    }
 }
     
index 9c3a1ed..6667422 100755 (executable)
@@ -12,7 +12,6 @@ public class LogicStatement {
         if (left == null) {
             throw new IRException();
         }
-
         Set set = left.getInversedRelations();
         if (right != null) {
             set.addAll(right.getInversedRelations());
@@ -20,6 +19,21 @@ public class LogicStatement {
         return set;
     }
     
+    public DNFConstraint constructDNF() {
+       if (op==AND) {
+           DNFConstraint leftd=left.constructDNF();
+           DNFConstraint rightd=right.constructDNF();
+           return leftd.and(rightd);
+       } else if (op==OR) {
+           DNFConstraint leftd=left.constructDNF();
+           DNFConstraint rightd=right.constructDNF();
+           return leftd.or(rightd);
+       } else if (op==NOT) {
+           DNFConstraint leftd=left.constructDNF();
+           return leftd.not();
+       } else throw new Error();
+    }
+
     public static class Operation {
         private final String name;
         private Operation(String opname) { name = opname; }
index 315c9fa..b576cbd 100755 (executable)
@@ -16,6 +16,23 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public DNFRule constructDNF() {
+        if (opcode==Opcode.AND) {
+            DNFRule leftd=left.constructDNF();
+            DNFRule rightd=right.constructDNF();
+            return leftd.and(rightd);
+        } else if (opcode==Opcode.OR) {
+            DNFRule leftd=left.constructDNF();
+            DNFRule rightd=right.constructDNF();
+            return leftd.or(rightd);
+        } else if (opcode==Opcode.NOT) {
+            DNFRule leftd=left.constructDNF();
+            return leftd.not();
+        } else throw new Error();
+    }
+
+
+
     public Set getInversedRelations() {
         Set set = left.getInversedRelations();
         if (right != null) {
index 9b739ff..ec465a4 100755 (executable)
@@ -6,7 +6,6 @@ import java.util.*;
 public class Optimizer {
 
     State state;
-
     public Optimizer(State s) {
         state = s;
     }
index 6c1539e..7ab2179 100755 (executable)
@@ -4,5 +4,9 @@ import java.util.*;
 
 public abstract class Predicate extends LogicStatement {
     protected Predicate() {}
+    public DNFConstraint constructDNF() {
+       return new DNFConstraint(this);
+    }
+    public int[] getRepairs(boolean negated) {}
 }
     
diff --git a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
new file mode 100755 (executable)
index 0000000..c1aa03b
--- /dev/null
@@ -0,0 +1,43 @@
+package MCC.IR;
+import java.util.*;
+
+public class RuleConjunction {
+
+    Vector predicates;
+    public RuleConjunction(DNFExpr pred) {
+       predicates=new Vector();
+       predicates.add(pred);
+    }
+    RuleConjunction(Vector preds){
+       predicates=preds       ;
+    }
+
+    int size() {
+       return predicates.size();
+    }
+    
+    DNFExpr get(int i) {
+       return (DNFExpr) predicates.get(i);
+    }
+
+    void add(DNFExpr dp) {
+       predicates.add(dp);
+    }
+
+    public RuleConjunction append(RuleConjunction c) {
+       RuleConjunction copy=copy();
+       for(int i=0;i<c.size();i++) {
+           copy.add(new DNFExpr(c.get(i)));
+       }
+       return copy;
+    }
+
+    public RuleConjunction copy() {
+       Vector vector=new Vector();
+       for (int i=0;i<=size();i++) {
+           DNFExpr dp=get(i);
+           vector.add(new DNFExpr(dp));
+       }
+       return new RuleConjunction(vector);
+    }
+}
index ae6b665..265663c 100755 (executable)
@@ -389,8 +389,8 @@ public class SemanticChecker {
         }
 
         /* do any post checks... (type constraints, etc?) */
-         
-        return ok;
+
+       return ok;
     }
 
     private boolean parse_constraint(ParseNode pn) {
@@ -527,7 +527,6 @@ public class SemanticChecker {
         } else {
             throw new IRException("not supported yet");
         }
-
     }
 
     private LogicStatement parse_body(ParseNode pn) {
diff --git a/Repair/RepairCompiler/MCC/IR/SetAnalysis.java b/Repair/RepairCompiler/MCC/IR/SetAnalysis.java
new file mode 100755 (executable)
index 0000000..7717ca6
--- /dev/null
@@ -0,0 +1,76 @@
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class SetAnalysis {
+    State state;
+    Hashtable intersection;
+    Hashtable subset;
+    Hashtable superset;
+
+    public SetAnalysis(State state) {
+       this.state=state;
+       intersection=new Hashtable();
+       subset=new Hashtable();
+       superset=new Hashtable();
+       doanalysis();
+    }
+
+    public Set getSuperset(SetDescriptor set1) {
+       return (Set)superset.get(set1);
+    }
+
+    public boolean isSubset(SetDescriptor set1, SetDescriptor set2) {
+       return subset.contains(set1)&&((Set)subset.get(set1)).contains(set2);
+    }
+
+    public boolean noIntersection(SetDescriptor set1, SetDescriptor set2) {
+       return intersection.contains(set1)&&((Set)intersection.get(set1)).contains(set2);
+    }
+    
+    void doanalysis() {
+       SymbolTable sets=state.stSets;
+       Vector descriptors=sets.getAllDescriptors();
+       for(int i=0;i<descriptors.size();i++) {
+           SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+           Stack st=new Stack();
+           st.addAll(sd.getSubsets());
+           while(!st.empty()) {
+               SetDescriptor subsetsd=(SetDescriptor)st.pop();
+               System.out.print(subsetsd.toString());
+
+               st.addAll(subsetsd.getSubsets());
+               if (!subset.contains(sd))
+                   subset.put(sd,new HashSet());
+               ((HashSet)subset.get(sd)).addAll(subsetsd.getSubsets());
+               for(Iterator it=subsetsd.getSubsets().iterator();it.hasNext();) {
+                   SetDescriptor sd2=(SetDescriptor)it.next();
+                   if (!superset.contains(sd2))
+                       superset.put(sd2,new HashSet());
+                   ((HashSet)superset.get(sd2)).add(sd);
+               }
+           }
+       }
+       for(int i=0;i<descriptors.size();i++) {
+           SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+           if (sd.isPartition()) {
+               Vector subst=sd.getSubsets();
+               for(Iterator it1=subst.iterator();it1.hasNext();) {
+                   SetDescriptor sd1=(SetDescriptor)it1.next();
+                   for(Iterator it2=subst.iterator();it2.hasNext();) {
+                       SetDescriptor sd2=(SetDescriptor)it2.next();
+                       if (sd1!=sd2) {
+                           for(Iterator it3=sd1.allSubsets().iterator();it3.hasNext();) {
+                               SetDescriptor sd3=(SetDescriptor)it3.next();
+                               
+                               if (!intersection.contains(sd3))
+                                   intersection.put(sd3,new HashSet());
+                               ((HashSet)intersection.get(sd3)).addAll(sd2.allSubsets());
+                           }
+                       }
+                   }
+               }
+           }
+       }
+    }
+}
index fee9795..4d375ac 100755 (executable)
@@ -22,6 +22,29 @@ public class SizeofPredicate extends Predicate {
         this.cardinality = cardinality;
     }
 
+    public int[] getRepairs(boolean negated) {
+       if (setexpr instanceof ImageSetExpr) {
+           if (opcode==Opcode.EQ)
+               return new int[] {AbstractRepair.ADDTORELATION,
+                                     AbstractRepair.REMOVEFROMRELATION};
+           if (((opcode==Opcode.GE)&&!negated)||
+               ((opcode==Opcode.LE)&&negated))
+               return new int[]{AbstractRepair.ADDTORELATION};
+           else
+               return new int[]{AbstractRepair.REMOVEFROMRELATION};
+       } else {
+           if (opcode==Opcode.EQ)
+               return new int[] {AbstractRepair.ADDTOSET,
+                                     AbstractRepair.REMOVEFROMSET};
+
+           if (((opcode==Opcode.GE)&&!negated)||
+               ((opcode==Opcode.LE)&&negated))
+               return new int[] {AbstractRepair.ADDTOSET};
+           else 
+               return new int[] {AbstractRepair.REMOVEFROMSET};
+       }
+    }
+
     public Set getRequiredDescriptors() {
         assert setexpr != null;
         Set v = setexpr.getRequiredDescriptors();
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
new file mode 100755 (executable)
index 0000000..14d144a
--- /dev/null
@@ -0,0 +1,93 @@
+package MCC.IR;
+import java.util.*;
+
+class Termination {
+    HashSet conjunctions;
+    Hashtable conjunctionmap;
+
+    HashSet abstractrepair;
+
+    State state;
+
+    public Termination(State state) {
+       this.state=state;
+       generateconjunctionnodes();
+       generaterepairnodes();
+    }
+    
+    void generateconjunctionnodes() {
+       Vector constraints=state.vConstraints;
+       for(int i=0;i<constraints.size();i++) {
+           Constraint c=(Constraint)constraints.get(i);
+           DNFConstraint dnf=c.dnfconstraint;
+           for(int j=0;j<dnf.size();j++) {
+               TermNode tn=new TermNode(c,dnf.get(j));
+               GraphNode gn=new GraphNode("Conjunction"+i+","+j,tn);
+               conjunctions.add(gn);
+               conjunctionmap.put(c,gn);
+           }
+       }
+    }
+
+    void generaterepairnodes() {
+       for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+           GraphNode gn=(GraphNode)conjiterator.next();
+           TermNode tn=(TermNode)gn.getOwner();
+           Conjunction conj=tn.getConjunction();
+           for(int i=0;i<conj.size();i++) {
+               DNFPredicate dp=conj.get(i);
+               int[] array=dp.getPredicate().getRepairs();
+               for {int j=0;j<array.length;j++) {
+                   AbstractRepair ar=new AbstractRepair(dp,array[j]);
+                   TermNode tn=new TermNode(ar);
+                   GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
+                   Edge e=new Edge("abstract",gn2);
+                   gn.addEdge(e);
+                   abstractrepair.add(gn2);
+               }
+           }
+       }
+    }
+}
+
+class AbstractRepair {
+    public final static int ADDTOSET=1;
+    public final static int REMOVEFROMSET=2;
+    public final static int ADDTORELATION=3;
+    public final static int REMOVEFROMRELATION=4;
+    public final static int MODIFYRELATION=5;
+
+    DNFPredicate torepair;
+    int type;
+
+    public AbstractRepair(DNFPredicate dp,int typ) {
+       torepair=dp;
+       type=typ;
+    }
+}
+
+class TermNode {
+    public final static int CONJUNCTION=1;
+    public final static int ABSTRACT=2;
+
+    Constraint constr;
+    Conjunction conj;
+    int type;
+    AbstractRepair repair;
+
+    public TermNode(Constraint constr, Conjunction conj) {
+       this.constr=constr;
+       this.conj=conj;
+       type=CONJUNCTION;
+    }
+
+    public TermNode(AbstractRepair ar) {
+       repair=ar;
+       type=ABSTRACT;
+    }
+
+    public Conjunction getConjunction() {
+       return conj;
+    }
+}
+