From: bdemsky <bdemsky>
Date: Mon, 5 Jan 2004 19:02:34 +0000 (+0000)
Subject: Still adding code to construct termination graph, abstract repair actions, concrete... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=cd8c06f13c3d628b15f745790e3eeac2891c5736;p=repair.git

Still adding code to construct termination graph, abstract repair actions, concrete repair actions, edge, etc...
---

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 5122d07..569485c 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -92,9 +92,93 @@ class AbstractInterferes {
 		    (neg2&&(op2==Opcode.LT)&&(size1a>=size2)))
 		    return false;
 	    } 
+	}
+	return true;
+    }
 
+    static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
+	if ((des!=dp.getPredicate().getDescriptor()) &&
+	    ((des instanceof SetDescriptor)||
+	     !dp.getPredicate().usesDescriptor((RelationDescriptor)des)))
+	    return false;
 
+	/* This if handles all the c comparisons in the paper */
+	if (des==dp.getPredicate().getDescriptor()&&
+	    (satisfy)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    {
+		if ((!neg2&&(op2==Opcode.GE))||
+		    (!neg2&&(op2==Opcode.GT))||
+		    (neg2&&(op2==Opcode.LE))||
+		    (neg2&&(op2==Opcode.LT)))
+		    return false;
+	    }
+	}
+	/* This if handles all the c comparisons in the paper */
+	if (des==dp.getPredicate().getDescriptor()&&
+	    (!satisfy)&&
+	    (dp.getPredicate() instanceof ExprPredicate)&&
+	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+	    boolean neg2=dp.isNegated();
+	    Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+	    int size2=((ExprPredicate)dp.getPredicate()).leftsize();
+	    {
+		if ((neg2&&(op2==Opcode.GE))||
+		    (neg2&&(op2==Opcode.GT))||
+		    (!neg2&&(op2==Opcode.LE))||
+		    (!neg2&&(op2==Opcode.LT)))
+		    return false;
+	    } 
 	}
 	return true;
     }
+
+    static public boolean interferes(Descriptor des, boolean satisfy, Rule r, boolean satisfyrule) {
+	for(int i=0;i<r.numQuantifiers();i++) {
+	    Quantifier q=r.getQuantifier(i);
+	    if (q instanceof RelationQuantifier||q instanceof SetQuantifier) {
+		if (q.getRequiredDescriptors().contains(des)&&(satisfy==satisfyrule))
+		    return true;
+	    } else if (q instanceof ForQuantifier) {
+		if (q.getRequiredDescriptors().contains(des))
+		    return true;
+	    } else throw new Error("Unrecognized Quantifier");
+	}
+	/* Scan DNF form */
+	DNFRule drule=r.getDNFGuardExpr();
+	for(int i=0;i<drule.size();i++) {
+	    RuleConjunction rconj=drule.get(i);
+	    for(int j=0;j<rconj.size();j++) {
+		DNFExpr dexpr=rconj.get(j);
+		Expr expr=dexpr.getExpr();
+		boolean negated=dexpr.getNegation();
+		/*
+		  satisfy  negated
+		  Yes      No             Yes
+		  Yes      Yes            No
+		  No       No             No
+		  No       Yes            Yes
+		*/
+		boolean satisfiesrule=(satisfy^negated);/*XOR of these */
+		if (satisfiesrule==satisfyrule) {
+		    /* Effect is the one being tested for */
+		    /* Only expr's to be concerned with are TupleOfExpr and
+		       ElementOfExpr */
+		    if (expr.getRequiredDescriptors().contains(des)) {
+			if (((expr instanceof ElementOfExpr)||
+			    (expr instanceof TupleOfExpr))&&
+			    (expr.getRequiredDescriptors().size()==1))
+			    return true;
+			else
+			    throw new Error("Unrecognized EXPR");
+		    }
+		}
+	    }
+	}
+	return false;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/Binding.java b/Repair/RepairCompiler/MCC/IR/Binding.java
new file mode 100755
index 0000000..585107c
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Binding.java
@@ -0,0 +1,20 @@
+package MCC.IR;
+
+class Binding {
+    VarDescriptor var;
+    int position;
+
+    public Binding(VarDescriptor vd,int pos) {
+	var=vd;
+	position=pos;
+    }
+
+    int getPosition() {
+	return position;
+    }
+
+    VarDescriptor getVar() {
+	return var;
+    }
+
+}
diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
new file mode 100755
index 0000000..d728062
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java
@@ -0,0 +1,24 @@
+package MCC.IR;
+
+class ConcreteInterferes {
+    static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
+	for(int i=0;i<mun.numUpdates();i++) {
+	    UpdateNode un=mun.getUpdate(i);
+	    for (int j=0;j<un.numUpdates();j++) {
+		Updates update=un.getUpdate(j);
+		Descriptor des=update.getDescriptor();
+		DNFRule drule=r.getDNFGuardExpr();
+		for(int k=0;k<drule.size();k++) {
+		    RuleConjunction rconj=drule.get(k);
+		    for(int l=0;l<rconj.size();l++) {
+			DNFExpr dexpr=rconj.get(l);
+			
+		    }
+		}
+	    }
+	}
+	return false;
+    }
+
+
+}
diff --git a/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java b/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java
new file mode 100755
index 0000000..17b8385
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/ConsequenceNode.java
@@ -0,0 +1,6 @@
+package MCC.IR;
+
+class ConsequenceNode {
+    public ConsequenceNode() {
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 1f3849f..4aff0d5 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -63,7 +63,7 @@ public class DNFConstraint {
     public DNFConstraint not() {
 	DNFConstraint copy=copy();
 	for (int i=0;i<size();i++) {
-	    Conjunction conj=get(i);
+	    Conjunction conj=copy.get(i);
 	    for (int j=0;j<conj.size();j++) {
 		DNFPredicate dp=conj.get(j);
 		dp.negatePred();
diff --git a/Repair/RepairCompiler/MCC/IR/DNFExpr.java b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
index ce039db..ac5d8be 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFExpr.java
@@ -16,4 +16,12 @@ public class DNFExpr {
     void negatePred() {
 	negate=!negate;
     }
+
+    public Expr getExpr() {
+	return predicate;
+    }
+
+    public boolean getNegation() {
+	return negate;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/DNFRule.java b/Repair/RepairCompiler/MCC/IR/DNFRule.java
index 942f7f6..ab76f57 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFRule.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFRule.java
@@ -63,7 +63,7 @@ public class DNFRule {
     public DNFRule not() {
 	DNFRule copy=copy();
 	for (int i=0;i<size();i++) {
-	    RuleConjunction conj=get(i);
+	    RuleConjunction conj=copy.get(i);
 	    for (int j=0;j<conj.size();j++) {
 		DNFExpr dp=conj.get(j);
 		dp.negatePred();
diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index 5336065..bf911bd 100755
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -20,10 +20,29 @@ public class DotExpr extends Expr {
     }
     */
 
+    FieldDescriptor fd;
+    TypeDescriptor fieldtype;
+    Expr intindex;
+    
     public DotExpr(Expr left, String field, Expr index) {
         this.left = left;
         this.field = field;
         this.index = index;
+
+        FieldDescriptor fd = struct.getField(field);
+        LabelDescriptor ld = struct.getLabel(field);        
+       if (ld != null) { /* label */
+            assert fd == null;
+            fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
+            fd = ld.getField();
+            assert fd != null;
+            assert intindex == null;
+            intindex = ld.getIndex();
+        } else {
+            fieldtype = fd.getType();
+	    intindex=index;
+        }
+	this.fd=fd;
     }
 
     public Set getRequiredDescriptors() {
@@ -32,7 +51,6 @@ public class DotExpr extends Expr {
         if (index != null) {
             v.addAll(index.getRequiredDescriptors());
         }
-
         return v;
     }
 
@@ -40,6 +58,14 @@ public class DotExpr extends Expr {
         return left;
     }
 
+    public FieldDescriptor getField() {
+	return fd;
+    }
+
+    public Expr getIndex() {
+	return intindex;
+    }
+
     public void generate(CodeWriter writer, VarDescriptor dest) {
         VarDescriptor leftd = VarDescriptor.makeNew("left");
 
@@ -54,23 +80,9 @@ public class DotExpr extends Expr {
         writer.outputline("");
       
         StructureTypeDescriptor struct = (StructureTypeDescriptor) left.getType();        
-        FieldDescriptor fd = struct.getField(field);
-        LabelDescriptor ld = struct.getLabel(field);        
-        TypeDescriptor fieldtype;
         Expr intindex = index;
         Expr offsetbits;
 
-        if (ld != null) { /* label */
-            assert fd == null;
-            fieldtype = ld.getType(); // d.s ==> Superblock, while,  d.b ==> Block
-            fd = ld.getField();
-            assert fd != null;
-            assert intindex == null;
-            intindex = ld.getIndex();
-        } else {
-            fieldtype = fd.getType();
-        }
-
         // #ATTN#: getOffsetExpr needs to be called with the fielddescriptor obect that is in teh vector list
         // this means that if the field is an arraydescriptor you have to call getOffsetExpr with the array 
         // descriptor not the underlying field descriptor
diff --git a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
index e4150d2..5739d63 100755
--- a/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/ForQuantifier.java
@@ -14,13 +14,21 @@ public class ForQuantifier extends Quantifier {
         this.var = vd;
     }
 
+    public VarDescriptor getVar() {
+	return var;
+    }
+
+
     public void setBounds(Expr lower, Expr upper) {
         this.lower = lower;
         this.upper = upper;
     }
 
     public Set getRequiredDescriptors() {
-        return new HashSet();
+        HashSet set=new HashSet();
+	set.addAll(lower.getRequiredDescriptors());
+	set.addAll(upper.getRequiredDescriptors());
+	return set;
     }
 
     public String toString() {
diff --git a/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
new file mode 100755
index 0000000..fdddbeb
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/MultUpdateNode.java
@@ -0,0 +1,23 @@
+package MCC.IR;
+import java.util.*;
+
+class MultUpdateNode {
+    Vector updates;
+    AbstractRepair abstractrepair;
+    public MultUpdateNode(AbstractRepair ar) {
+	updates=new Vector();
+	abstractrepair=ar;
+    }
+    void addUpdate(UpdateNode un) {
+	updates.add(un);
+    }
+    int numUpdates() {
+	return updates.size();
+    }
+    AbstractRepair getRepair() {
+	return abstractrepair;
+    }
+    UpdateNode getUpdate(int i) {
+	return (UpdateNode)updates.get(i);
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java
index 47a6fae..b3af827 100755
--- a/Repair/RepairCompiler/MCC/IR/OpExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java
@@ -16,6 +16,10 @@ public class OpExpr extends Expr {
         assert (right == null && opcode == Opcode.NOT) || (right != null);
     }
 
+    public Opcode getOpcode() {
+	return opcode;
+    }
+
     public DNFRule constructDNF() {
         if (opcode==Opcode.AND) {
             DNFRule leftd=left.constructDNF();
@@ -28,7 +32,7 @@ public class OpExpr extends Expr {
         } else if (opcode==Opcode.NOT) {
             DNFRule leftd=left.constructDNF();
             return leftd.not();
-        } else throw new Error();
+        } else return new DNFRule(this);
     }
 
     public boolean usesDescriptor(RelationDescriptor rd) {
diff --git a/Repair/RepairCompiler/MCC/IR/Quantifier.java b/Repair/RepairCompiler/MCC/IR/Quantifier.java
index 3f302b8..2f5c170 100755
--- a/Repair/RepairCompiler/MCC/IR/Quantifier.java
+++ b/Repair/RepairCompiler/MCC/IR/Quantifier.java
@@ -3,7 +3,6 @@ package MCC.IR;
 import java.util.*;
 
 public abstract class Quantifier {
-
     public abstract Set getRequiredDescriptors();
 
     public abstract void generate_open(CodeWriter writer);
diff --git a/Repair/RepairCompiler/MCC/IR/Rule.java b/Repair/RepairCompiler/MCC/IR/Rule.java
index 69e8d0d..12650d9 100755
--- a/Repair/RepairCompiler/MCC/IR/Rule.java
+++ b/Repair/RepairCompiler/MCC/IR/Rule.java
@@ -12,7 +12,8 @@ public class Rule {
     Expr guard = null;
     Inclusion inclusion = null;    
     SymbolTable st = new SymbolTable();
-    
+    DNFRule dnfguard=null,dnfnegguard=null;
+
     String label;
     
     int num;
@@ -22,6 +23,14 @@ public class Rule {
         label = new String("rule" + count++);
     }
     
+    public int numQuantifiers() {
+	return quantifiers.size();
+    }
+
+    public Quantifier getQuantifier(int i) {
+	return (Quantifier) quantifiers.get(i);
+    }
+
     public int getNum() {
         return num;
     }
@@ -48,12 +57,23 @@ public class Rule {
 
     public void setGuardExpr(Expr guard) {
         this.guard = guard;
+	dnfguard=guard.constructDNF();
+	OpExpr opexpr=new OpExpr(Opcode.NOT,guard,null);
+	dnfnegguard=opexpr.constructDNF();
     }
     
     public Expr getGuardExpr() {
         return guard;
     }
 
+    public DNFRule getDNFGuardExpr() {
+        return dnfguard;
+    }
+
+    public DNFRule getDNFNegGuardExpr() {
+        return dnfnegguard;
+    }
+
     public void setInclusion(Inclusion inclusion) {
         this.inclusion = inclusion;
     }
diff --git a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
index c1aa03b..b2723bc 100755
--- a/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
+++ b/Repair/RepairCompiler/MCC/IR/RuleConjunction.java
@@ -34,7 +34,7 @@ public class RuleConjunction {
 
     public RuleConjunction copy() {
 	Vector vector=new Vector();
-	for (int i=0;i<=size();i++) {
+	for (int i=0;i<size();i++) {
 	    DNFExpr dp=get(i);
 	    vector.add(new DNFExpr(dp));
 	}
diff --git a/Repair/RepairCompiler/MCC/IR/ScopeNode.java b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
index 8a10b6d..168117d 100755
--- a/Repair/RepairCompiler/MCC/IR/ScopeNode.java
+++ b/Repair/RepairCompiler/MCC/IR/ScopeNode.java
@@ -8,4 +8,15 @@ class ScopeNode {
 	rule=r;
 	this.satisfy=satisfy;
     }
+    public Descriptor getDescriptor() {
+	Inclusion inc=rule.getInclusion();
+	if (inc instanceof SetInclusion)
+	    return ((SetInclusion)inc).getSet();
+	else if (inc instanceof RelationInclusion)
+	    return ((RelationInclusion)inc).getRelation();
+	else throw new Error("Unrecognized Inclusion");
+    }
+    public boolean getSatisfy() {
+	return satisfy;
+    }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/TermNode.java b/Repair/RepairCompiler/MCC/IR/TermNode.java
index 46b9f74..9e3dbe8 100755
--- a/Repair/RepairCompiler/MCC/IR/TermNode.java
+++ b/Repair/RepairCompiler/MCC/IR/TermNode.java
@@ -5,14 +5,15 @@ class TermNode {
     public final static int ABSTRACT=2;
     public final static int UPDATE=3;
     public final static int RULESCOPE=4;
-    
+    public final static int CONSEQUENCE=5;
 
+    ConsequenceNode conseqnode;
     Constraint constr;
     Conjunction conj;
     int type;
     AbstractRepair repair;
     ScopeNode scope;
-
+    MultUpdateNode update;
 
     public TermNode(Constraint constr, Conjunction conj) {
 	this.constr=constr;
@@ -25,11 +26,28 @@ class TermNode {
 	type=ABSTRACT;
     }
 
+    public TermNode(ConsequenceNode cn) {
+	conseqnode=cn;
+	type=CONSEQUENCE;
+    }
+
     public TermNode(ScopeNode sn) {
 	scope=sn;
 	type=RULESCOPE;
     }
 
+    public TermNode(MultUpdateNode un) {
+	update=un;
+	type=UPDATE;
+    }
+
+    public ConsequenceNode getConsequence() {
+	if (type!=CONSEQUENCE)
+	    throw new Error("Not Consequence Node!");
+	else
+	    return conseqnode;
+    }
+
     public Conjunction getConjunction() {
 	if (type!=CONJUNCTION)
 	    throw new Error("Not Conjunction Node!");
@@ -37,6 +55,20 @@ class TermNode {
 	    return conj;
     }
 
+    public MultUpdateNode getUpdate() {
+	if (type!=UPDATE)
+	    throw new Error("Not Update Node!");
+	else
+	    return update;
+    }
+
+    public ScopeNode getScope() {
+	if (type!=RULESCOPE)
+	    throw new Error("Not Scope Node!");
+	else
+	    return scope;
+    }
+
     public AbstractRepair getAbstract() {
 	if (type!=ABSTRACT)
 	    throw new Error("Not Abstract Repair Node!");
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 7f9adc0..bfbe8db 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -1,5 +1,6 @@
 package MCC.IR;
 import java.util.*;
+import java.io.*;
 import MCC.State;
 
 public class Termination {
@@ -7,10 +8,13 @@ public class Termination {
     Hashtable conjunctionmap;
 
     HashSet abstractrepair;
+    HashSet updatenodes;
+    HashSet consequencenodes;
 
     HashSet scopenodes;
     Hashtable scopesatisfy;
     Hashtable scopefalsify;
+    Hashtable consequence;
 
     State state;
 
@@ -22,12 +26,31 @@ public class Termination {
 	scopenodes=new HashSet();
 	scopesatisfy=new Hashtable();
 	scopefalsify=new Hashtable();
+	consequence=new Hashtable();
+	updatenodes=new HashSet();
+	consequencenodes=new HashSet();
 
 	generateconjunctionnodes();
+	generatescopenodes();
 	generaterepairnodes();
-	generateabstractedges();
 	generatedatastructureupdatenodes();
-	generatescopenodes();
+
+	generateabstractedges();
+	generatescopeedges();
+	generateupdateedges();
+
+	HashSet superset=new HashSet();
+	superset.addAll(conjunctions);
+	superset.addAll(abstractrepair);
+	superset.addAll(updatenodes);
+	superset.addAll(scopenodes);
+	superset.addAll(consequencenodes);
+	try {
+	    GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
+	} catch (Exception e) {
+	    e.printStackTrace();
+	    System.exit(-1);
+	}
     }
     
     void generateconjunctionnodes() {
@@ -37,13 +60,37 @@ public class Termination {
 	    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);
+		GraphNode gn=new GraphNode("Conjunction"+i+"B"+j,tn);
 		conjunctions.add(gn);
 		conjunctionmap.put(c,gn);
 	    }
 	}
     }
 
+    void generateupdateedges() {
+	for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
+	    GraphNode gn=(GraphNode)updateiterator.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    MultUpdateNode mun=tn.getUpdate();
+	    /* Cycle through the rules to look for possible conflicts */
+	    for(int i=0;i<state.vRules.size();i++) {
+		Rule r=(Rule) state.vRules.get(i);  
+		if (ConcreteInterferes.interferes(mun,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 (ConcreteInterferes.interferes(mun,r,false)) {
+		    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
+		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+		    GraphNode gnconseq=(GraphNode)consequence.get(sn);
+		    gnconseq.addEdge(e);
+		}
+	    }
+	}
+    }
+
     void generateabstractedges() {
 	for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 	    GraphNode gn=(GraphNode)absiterator.next();
@@ -66,6 +113,47 @@ public class Termination {
 	}
     }
     
+    void generatescopeedges() {
+	for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
+	    GraphNode gn=(GraphNode)scopeiterator.next();
+	    TermNode tn=(TermNode)gn.getOwner();
+	    ScopeNode sn=tn.getScope();
+	    
+	    /* Interference edges with conjunctions */
+	    for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+		GraphNode gn2=(GraphNode)conjiterator.next();
+		TermNode tn2=(TermNode)gn2.getOwner();
+		Conjunction conj=tn2.getConjunction();
+		for(int i=0;i<conj.size();i++) {
+		    DNFPredicate dp=conj.get(i);
+		    if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
+			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+			GraphNode gnconseq=(GraphNode)consequence.get(sn);
+			gnconseq.addEdge(e);
+			break;
+		    }
+		}
+	    }
+
+	    /* 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)) {
+		    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)) {
+		    GraphNode scopenode=(GraphNode)scopefalsify.get(r);
+		    GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+		    GraphNode gnconseq=(GraphNode)consequence.get(sn);
+		    gnconseq.addEdge(e);
+		}
+	    }
+	}
+    }
+
 
     void generaterepairnodes() {
 	for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
@@ -79,7 +167,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()+"-"+i+","+j,tn2);
+		    GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+j,tn2);
 		    GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 		    gn.addEdge(e);
 		    abstractrepair.add(gn2);
@@ -94,27 +182,212 @@ public class Termination {
 	    TermNode tn=(TermNode) gn.getOwner();
 	    AbstractRepair ar=tn.getAbstract();
 	    if (ar.getType()==AbstractRepair.ADDTOSET) {
-		generateaddtoset(ar);
+		generateaddtoset(gn,ar);
 	    } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
-		generateremovefromset(ar);
+		generateremovefromset(gn,ar);
 	    } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
-		generateaddtorelation(ar);
+		generateaddtorelation(gn,ar);
 	    } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
-		generateremovefromrelation(ar);
+		generateremovefromrelation(gn,ar);
 	    } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
-		generatemodifyrelation(ar);
+		generatemodifyrelation(gn,ar);
 	    }
 	}
     }
 
-    void generateaddtoset(AbstractRepair ar) {
+    void generateremovefromset(GraphNode gn,AbstractRepair ar) {
+	Vector possiblerules=new Vector();
+	for(int i=0;i<state.vRules.size();i++) {
+	    Rule r=(Rule) state.vRules.get(i);
+	    if ((r.getInclusion() instanceof SetInclusion)&&
+		(ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
+		possiblerules.add(r);
+	}
+	int[] count=new int[possiblerules.size()];
+	while(remains(count,possiblerules)) {
+	    MultUpdateNode mun=new MultUpdateNode(ar);
+	    for(int i=0;i<possiblerules.size();i++) {
+		UpdateNode un=new UpdateNode();
+		mun.addUpdate(un);
+		/* CODE HERE*/
+	    }
+	    increment(count,possiblerules);
+	}
+    }
+
+    static void increment(int count[], Vector rules) {
+	count[0]++;
+	for(int i=0;i<(rules.size()-1);i++) {
+	    if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+		count[i+1]++;
+		count[i]=0;
+	    } else break;
+	}
+    }
+
+    static boolean remains(int count[], Vector rules) {
+	for(int i=0;i<rules.size();i++) {
+	    if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+		return false;
+	    }
+	}
+	return true;
+    }
+
+    void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {}
+    void generateaddtorelation(GraphNode gn,AbstractRepair ar) {}
+    void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {}
+
+    static int addtocount=0;
+    void generateaddtoset(GraphNode gn, AbstractRepair ar) {
 	for(int i=0;i<state.vRules.size();i++) {
 	    Rule r=(Rule) state.vRules.get(i);
 	    if (r.getInclusion() instanceof SetInclusion) {
 		if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
 		    //Generate add instruction
-		    
-
+		    DNFRule dnfrule=r.getDNFGuardExpr();
+		    for(int j=0;j<dnfrule.size();j++) {
+			Inclusion inc=r.getInclusion();
+			UpdateNode un=new UpdateNode();
+			/* First solve for quantifiers */
+			boolean goodupdate=true;
+			for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
+			    Quantifier q=(Quantifier)iterator.next();
+			    boolean foundall=true;
+			    if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
+				VarDescriptor vd=null;
+				if (q instanceof SetQuantifier)
+				    vd=((SetQuantifier)q).getVar();
+				else
+				    vd=((ForQuantifier)q).getVar();
+				if(inc instanceof SetInclusion) {
+				    SetInclusion si=(SetInclusion)inc;
+				    if ((si.elementexpr instanceof VarExpr)&&
+					(((VarExpr)si.elementexpr).getVar()==vd)) {
+					/* Can solve for v */
+					Binding binding=new Binding(vd,0);
+					un.addBinding(binding);
+				    } else
+					foundall=false;
+				} else if (inc instanceof RelationInclusion) {
+				    RelationInclusion ri=(RelationInclusion)inc;
+				    boolean f1=true;
+				    boolean f2=true;
+				    if ((ri.getLeftExpr() instanceof VarExpr)&&
+					(((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+					/* Can solve for v */
+					Binding binding=new Binding(vd,0);
+					un.addBinding(binding);
+				    } else f1=false;
+				    if ((ri.getRightExpr() instanceof VarExpr)&&
+					(((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+					/* Can solve for v */
+					Binding binding=new Binding(vd,0);
+					un.addBinding(binding);
+				    } else f2=false;
+				    if (!(f1||f2))
+					foundall=false;
+				} else throw new Error("Inclusion not recognized");
+			    } else if (q instanceof RelationQuantifier) {
+				RelationQuantifier rq=(RelationQuantifier)q;
+				for(int k=0;k<2;k++) {
+				    VarDescriptor vd=(k==0)?rq.x:rq.y;
+				    if(inc instanceof SetInclusion) {
+					SetInclusion si=(SetInclusion)inc;
+					if ((si.elementexpr instanceof VarExpr)&&
+					    (((VarExpr)si.elementexpr).getVar()==vd)) {
+					    /* Can solve for v */
+					    Binding binding=new Binding(vd,0);
+					    un.addBinding(binding);
+					} else
+					    foundall=false;
+				    } else if (inc instanceof RelationInclusion) {
+					RelationInclusion ri=(RelationInclusion)inc;
+					boolean f1=true;
+					boolean f2=true;
+					if ((ri.getLeftExpr() instanceof VarExpr)&&
+					    (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
+					    /* Can solve for v */
+					    Binding binding=new Binding(vd,0);
+					    un.addBinding(binding);
+					} else f1=false;
+					if ((ri.getRightExpr() instanceof VarExpr)&&
+						   (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
+					    /* Can solve for v */
+					    Binding binding=new Binding(vd,0);
+					    un.addBinding(binding);
+					} else f2=false;
+					if (!(f1||f2))
+					    foundall=false;
+				    } else throw new Error("Inclusion not recognized");
+				}
+			    } else throw new Error("Quantifier not recognized");
+			    if (!foundall) {
+				goodupdate=false;
+				break;
+			    }
+			    /* Now build update for tuple/set inclusion condition */
+			    if(inc instanceof SetInclusion) {
+				SetInclusion si=(SetInclusion)inc;
+				if (!(si.elementexpr instanceof VarExpr)) {
+				    Updates up=new Updates(si.elementexpr,0);
+				    un.addUpdate(up);
+				}
+			    } 
+			    if (inc instanceof RelationInclusion) {
+				RelationInclusion ri=(RelationInclusion)inc;
+				if (!(ri.getLeftExpr() instanceof VarExpr)) {
+				    Updates up=new Updates(ri.getLeftExpr(),0);
+				    un.addUpdate(up);
+				}
+				if (!(ri.getRightExpr() instanceof VarExpr)) {
+				    Updates up=new Updates(ri.getRightExpr(),0);
+				    un.addUpdate(up);
+				}
+			    }
+			    //Finally build necessary updates to satisfy conjunction
+			    RuleConjunction ruleconj=dnfrule.get(j);
+			    for(int k=0;k<ruleconj.size();k++) {
+				DNFExpr de=ruleconj.get(k);
+				Expr e=de.getExpr();
+				if (e instanceof OpExpr) {
+				    OpExpr ex=(OpExpr)de.getExpr();
+				    Opcode op=ex.getOpcode();
+				    if (de.getNegation()) {
+					/* remove negation through opcode translation */
+					if (op==Opcode.GT)
+					    op=Opcode.LE;
+					else if (op==Opcode.GE)
+					    op=Opcode.LT;
+					else if (op==Opcode.EQ)
+					    op=Opcode.NE;
+					else if (op==Opcode.NE)
+					    op=Opcode.EQ;
+					else if (op==Opcode.LT)
+					    op=Opcode.GE;
+					else if (op==Opcode.LE)
+					    op=Opcode.GT;
+				    }
+				    Updates up=new Updates(ex.left,ex.right,op);
+				    un.addUpdate(up);
+				} else if (e instanceof ElementOfExpr) {
+				    Updates up=new Updates(e,de.getNegation());
+				    un.addUpdate(up);
+				} else if (e instanceof TupleOfExpr) {
+				    Updates up=new Updates(e,de.getNegation());
+				    un.addUpdate(up);
+				} else throw new Error("Error #213");
+			    }
+			}
+			MultUpdateNode mun=new MultUpdateNode(ar);
+			mun.addUpdate(un);
+			TermNode tn=new TermNode(mun);
+			GraphNode gn2=new GraphNode("Update"+addtocount,tn);
+			GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
+			addtocount++;
+			gn.addEdge(e);
+			updatenodes.add(gn2);
+		    }
 		}
 	    }
 	}
@@ -125,14 +398,28 @@ public class Termination {
 	    Rule r=(Rule) state.vRules.get(i);
 	    ScopeNode satisfy=new ScopeNode(r,true);
 	    TermNode tnsatisfy=new TermNode(satisfy);
-	    GraphNode gnsatisfy=new GraphNode("Satisfy Rule"+i,tnsatisfy);
+	    GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
+	    ConsequenceNode cnsatisfy=new ConsequenceNode();
+	    TermNode ctnsatisfy=new TermNode(cnsatisfy);
+	    GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
+	    consequence.put(satisfy,cgnsatisfy);
+	    GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
+	    gnsatisfy.addEdge(esat);
+	    consequencenodes.add(cgnsatisfy);
+	    scopesatisfy.put(r,gnsatisfy);
+	    scopenodes.add(gnsatisfy);
 
 	    ScopeNode falsify=new ScopeNode(r,false);
 	    TermNode tnfalsify=new TermNode(falsify);
-	    GraphNode gnfalsify=new GraphNode("Falsify Rule"+i,tnfalsify);
-	    scopesatisfy.put(r,gnsatisfy);
+	    GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
+	    ConsequenceNode cnfalsify=new ConsequenceNode();
+	    TermNode ctnfalsify=new TermNode(cnfalsify);
+	    GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
+	    consequence.put(falsify,cgnfalsify);
+	    GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
+	    gnfalsify.addEdge(efals);
+	    consequencenodes.add(cgnfalsify);
 	    scopefalsify.put(r,gnfalsify);
-	    scopenodes.add(gnsatisfy);
 	    scopenodes.add(gnfalsify);
 	}
     }
diff --git a/Repair/RepairCompiler/MCC/IR/UpdateNode.java b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
new file mode 100755
index 0000000..3a02c37
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/UpdateNode.java
@@ -0,0 +1,27 @@
+package MCC.IR;
+import java.util.*;
+
+class UpdateNode {
+    Vector updates;
+    Vector bindings;
+
+    public UpdateNode() {
+	updates=new Vector();
+	bindings=new Vector();
+    }
+
+    public void addBinding(Binding b) {
+	bindings.add(b);
+    }
+
+    public void addUpdate(Updates u) {
+	updates.add(u);
+    }
+
+    public int numUpdates() {
+	return updates.size();
+    }
+    public Updates getUpdate(int i) {
+	return (Updates)updates.get(i);
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java
new file mode 100755
index 0000000..7e4dbd3
--- /dev/null
+++ b/Repair/RepairCompiler/MCC/IR/Updates.java
@@ -0,0 +1,95 @@
+package MCC.IR;
+
+class Updates {
+    static public final int EXPR=0;
+    static public final int POSITION=1;
+    static public final int ABSTRACT=2;
+    int type=-1;
+    int rightposition;
+    Expr rightexpr;
+    Expr leftexpr;
+    Opcode opcode;
+    boolean negate;
+
+    public Updates(Expr lexpr, Expr rexpr, Opcode op) {
+	leftexpr=lexpr;
+	type=Updates.EXPR;
+	opcode=Opcode.EQ;
+	/* Get rid of everything but NE */
+	if (op==Opcode.GT) {
+	    rightexpr=new OpExpr(Opcode.ADD,rexpr,new IntegerLiteralExpr(1));
+	} else if (op==Opcode.GE) {
+	    rightexpr=rexpr;
+	} else if (op==Opcode.LT) {
+	    rightexpr=new OpExpr(Opcode.SUB,rexpr,new IntegerLiteralExpr(1));
+	} else if (op==Opcode.LE) {
+	    rightexpr=rexpr;
+	} else if (op==Opcode.EQ) {
+	    rightexpr=rexpr;
+	} else if (op==Opcode.NE) {
+	    opcode=Opcode.NE;
+	}
+    }
+
+    boolean isGlobal() {
+	if (leftexpr instanceof VarExpr)
+	    return true;
+	else return false;
+    }
+
+    Descriptor getDescriptor() {
+	if (isGlobal()) {
+	    return ((VarExpr)leftexpr).getVar();
+	} else if (isField()) {
+	    return ((DotExpr)leftexpr).getField();
+	} else throw New Error("Unrecognized Update");
+    }
+
+    boolean isField() {
+	if (leftexpr instanceof DotExpr) {
+	    assert ((DotExpr)leftexpr).getIndex()==null;
+	    return true;
+	} else
+	    return false;
+    }
+    
+    
+    Opcode getOpcode() {
+	return opcode;
+    }
+
+    public Updates(Expr lexpr, Expr rexpr) {
+	leftexpr=lexpr;
+	rightexpr=rexpr;
+	type=Updates.EXPR;
+	opcode=Opcode.EQ;
+    }
+
+    public Updates(Expr lexpr, int rpos) {
+	leftexpr=lexpr;
+	rightposition=rpos;
+	type=Updates.POSITION;
+	opcode=null;
+    }
+    public Updates(Expr lexpr,boolean negates) {
+	leftexpr=lexpr;
+	type=Updates.ABSTRACT;
+	negate=negates;
+	opcode=null;
+    }
+
+    public int getType() {
+	return type;
+    }
+    public Expr getLeftExpr() {
+	return leftexpr;
+    }
+    public int getRightPos() {
+	assert type==Updates.POSITION;
+	return rightposition;
+    }
+    public Expr getRightExpr() {
+	assert type==Updates.EXPR;
+	return rightexpr;
+    }
+}
diff --git a/Repair/RepairCompiler/MCC/Makefile b/Repair/RepairCompiler/MCC/Makefile
index b1d5648..59652ed 100755
--- a/Repair/RepairCompiler/MCC/Makefile
+++ b/Repair/RepairCompiler/MCC/Makefile
@@ -82,6 +82,7 @@ parser: $(PARSERS) $(SCANNER).java
 
 %.class: %.java
 	javac -classpath ../ -source 1.4 $<
+#	jikes -classpath $(CLASSPATH):../ $<
 
 %.lex.java: %.lex
 	java -classpath ../ JLex.Main $<