From a0a7e93f41239e9aa128e3441c3e71ffe2f47a3c Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Mon, 8 Nov 2004 01:48:32 +0000
Subject: [PATCH 1/1] Improved termination analysis so that daikon generated
 specifications won't have problems.

---
 .../MCC/IR/AbstractInterferes.java            | 161 ++++++++++++++++--
 Repair/RepairCompiler/MCC/IR/Constraint.java  |  17 +-
 .../RepairCompiler/MCC/IR/DNFConstraint.java  |  10 ++
 Repair/RepairCompiler/MCC/IR/Termination.java | 109 +++++++-----
 4 files changed, 232 insertions(+), 65 deletions(-)

diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
index 68ed221..df03933 100755
--- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
+++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
@@ -8,6 +8,7 @@ class AbstractInterferes {
 	termination=t;
     }
 
+
     /** Does performing the AbstractRepair ar satisfy (or falsify if satisfy=false)
      * Rule r. */
 
@@ -43,7 +44,7 @@ class AbstractInterferes {
 	    drule=r.getDNFGuardExpr();
 	else
 	    drule=r.getDNFNegGuardExpr();
-	
+
 	for(int i=0;i<drule.size();i++) {
 	    RuleConjunction rconj=drule.get(i);
 	    for(int j=0;j<rconj.size();j++) {
@@ -59,6 +60,10 @@ class AbstractInterferes {
 	return false;
     }
 
+    /** This method is designed to check that modifying a relation
+     * doesn't violate a relation well-formedness constraint
+     * (ie. [forall <a,b> in R], a in S1 and b in S2; */
+
     public boolean checkrelationconstraint(AbstractRepair ar, Constraint c) {
 	if (c.numQuantifiers()==1&&
 	    (c.getQuantifier(0) instanceof RelationQuantifier)) {
@@ -99,6 +104,137 @@ class AbstractInterferes {
 	return false;
     }
 
+
+    /** Check to see if performing the repair ar on repair_c does not
+     *  inferere with interfere_c.  Returns true if there is no
+     *  interference.  */
+
+    public boolean interferemodifies(AbstractRepair ar, Constraint repair_c, DNFPredicate interfere_pred, Constraint interfere_c) {
+        DNFConstraint precondition=repair_c.getDNFConstraint().not();
+        if (repair_c.numQuantifiers()!=1||
+            interfere_c.numQuantifiers()!=1||
+            !(repair_c.getQuantifier(0) instanceof SetQuantifier)||
+            !(interfere_c.getQuantifier(0) instanceof SetQuantifier)||
+            ((SetQuantifier)repair_c.getQuantifier(0)).getSet()!=((SetQuantifier)interfere_c.getQuantifier(0)).getSet())
+            return false;
+
+        Hashtable mapping=new Hashtable();
+        mapping.put(((SetQuantifier)repair_c.getQuantifier(0)).getVar(),
+                    ((SetQuantifier)interfere_c.getQuantifier(0)).getVar());
+
+        if (ar.getType()!=AbstractRepair.MODIFYRELATION||
+            !(ar.getPredicate().getPredicate() instanceof ExprPredicate)||
+            !(interfere_pred.getPredicate() instanceof ExprPredicate))
+            return false;
+        Expr e=((ExprPredicate)interfere_pred.getPredicate()).expr;
+        Expr leftside=((OpExpr)((ExprPredicate)ar.getPredicate().getPredicate()).expr).left;
+        Set relationset=e.useDescriptor(ar.getDescriptor());
+        for(Iterator relit=relationset.iterator();relit.hasNext();) {
+            Expr e2=(Expr)relit.next();
+            if (!leftside.equals(mapping,e2))
+                return false;
+        }
+        /* Prune precondition using any ar's in the same conjunction */
+        adjustcondition(precondition, ar);
+        Conjunction conj=findConjunction(repair_c.getDNFConstraint(),ar.getPredicate());
+        for(int i=0;i<conj.size();i++) {
+            DNFPredicate dp=conj.get(i);
+            Set s=(Set)termination.predtoabstractmap.get(dp);
+            for(Iterator it=s.iterator();it.hasNext();) {
+                GraphNode gn=(GraphNode)it.next();
+                TermNode tn=(TermNode)gn.getOwner();
+                AbstractRepair dp_ar=tn.getAbstract();
+                adjustcondition(precondition, dp_ar);
+            }
+        }
+        /* We now have precondition after interference */
+        if (precondition.size()==0)
+            return false;
+        DNFConstraint infr_const=interfere_c.getDNFConstraint();
+
+    next_conj:
+        for(int i=0;i<infr_const.size();i++) {
+            Conjunction infr_conj=infr_const.get(i);
+            for(int j=0;j<infr_conj.size();j++) {
+                DNFPredicate infr_dp=infr_conj.get(j);
+            next_pre_conj:
+                for(int i2=0;i2<precondition.size();i2++) {
+                    Conjunction pre_conj=precondition.get(i2);
+                    for(int j2=0;j2<pre_conj.size();j2++) {
+                        DNFPredicate pre_dp=pre_conj.get(j2);
+                        if (checkPreEnsures(pre_dp,infr_dp,mapping))
+                            continue next_pre_conj;
+
+                    }
+                    continue next_conj; /* The precondition doesn't ensure this conjunction is true */
+                }
+            }
+            return true; /*Found a conjunction that must be
+                           true...therefore the precondition
+                           guarantees that the second constraint is
+                           always true after repair*/
+        }
+        return false;
+    }
+
+    static private Conjunction findConjunction(DNFConstraint cons, DNFPredicate dp) {
+        for(int i=0;i<cons.size();i++) {
+            Conjunction conj=cons.get(i);
+            for(int j=0;j<conj.size();j++) {
+                DNFPredicate curr_dp=conj.get(j);
+                if (curr_dp==dp)
+                    return conj;
+            }
+        }
+        throw new Error("Not found");
+    }
+
+    /** This method removes predicates that the abstract repair may
+     *  violate. */
+
+    private void adjustcondition(DNFConstraint precond, AbstractRepair ar) {
+        HashSet conjremove=new HashSet();
+        for(int i=0;i<precond.size();i++) {
+            Conjunction conj=precond.get(i);
+            HashSet toremove=new HashSet();
+            for(int j=0;j<conj.size();j++) {
+                DNFPredicate dp=conj.get(j);
+                if (interfereswithpredicate(ar,dp)) {
+                    /* Remove dp from precond */
+                    toremove.add(dp);
+                }
+            }
+            conj.predicates.removeAll(toremove);
+            if (conj.size()==0)
+                conjremove.add(conj);
+        }
+        precond.conjunctions.removeAll(conjremove);
+    }
+
+    private boolean checkPreEnsures(DNFPredicate pre_dp,  DNFPredicate infr_dp, Hashtable mapping) {
+        if (pre_dp.isNegated()==infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
+            (infr_dp.getPredicate() instanceof ExprPredicate)) {
+            if (((ExprPredicate)pre_dp.getPredicate()).expr.equals(mapping, ((ExprPredicate)infr_dp.getPredicate()).expr))
+                return true;
+        }
+        if ((!pre_dp.isNegated())&&infr_dp.isNegated()&&(pre_dp.getPredicate() instanceof ExprPredicate)&&
+            (infr_dp.getPredicate() instanceof ExprPredicate)) {
+            ExprPredicate pre_ep=(ExprPredicate)pre_dp.getPredicate();
+            ExprPredicate infr_ep=(ExprPredicate)infr_dp.getPredicate();
+            if (pre_ep.getType()==ExprPredicate.COMPARISON&&
+                infr_ep.getType()==ExprPredicate.COMPARISON&&
+                pre_ep.isRightInt()&&
+                infr_ep.isRightInt()&&
+                pre_ep.rightSize()!=infr_ep.rightSize()&&
+                pre_ep.getOp()==Opcode.EQ&&
+                infr_ep.getOp()==Opcode.EQ) {
+                if (((OpExpr)pre_ep.expr).left.equals(mapping,((OpExpr)infr_ep.expr).left))
+                    return true;
+            }
+        }
+        return false;
+    }
+
     /** This method checks whether a modify relation abstract repair
      * to satisfy ar may violate dp.  It returns true if there is no
      * interference. */
@@ -106,19 +242,19 @@ class AbstractInterferes {
     private boolean interferemodifies(DNFPredicate ar,DNFPredicate dp) {
 	boolean neg1=ar.isNegated();
 	Opcode op1=((ExprPredicate)ar.getPredicate()).getOp();
-	Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;	
+	Expr rexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).right;
 	Expr lexpr1=((OpExpr)((ExprPredicate)ar.getPredicate()).expr).left;
 	RelationDescriptor updated_des=(RelationDescriptor)((ExprPredicate)ar.getPredicate()).getDescriptor();
-	
+
 	boolean neg2=dp.isNegated();
 	Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
 	Expr rexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 	Expr lexpr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left;
-	
+
 	/* Translate the opcodes */
 	op1=Opcode.translateOpcode(neg1,op1);
 	op2=Opcode.translateOpcode(neg2,op2);
-	
+
 	if (((op1==Opcode.EQ)||(op1==Opcode.GE)||(op1==Opcode.LE))&&
 	    ((op2==Opcode.EQ)||(op2==Opcode.GE)||(op2==Opcode.LE))&&
 	    !rexpr2.usesDescriptor(updated_des)) {
@@ -171,7 +307,8 @@ class AbstractInterferes {
 	return false;
     }
 
-    /** Does performing the AbstractRepair ar falsify the predicate dp */
+    /** Returns true if performing the AbstractRepair ar may falsify
+        the predicate dp. */
 
     public boolean interfereswithpredicate(AbstractRepair ar, DNFPredicate dp) {
 	if ((ar.getDescriptor()!=dp.getPredicate().getDescriptor()) &&
@@ -269,7 +406,7 @@ class AbstractInterferes {
 	    int size2=((ExprPredicate)dp.getPredicate()).rightSize();
 
 	    op2=Opcode.translateOpcode(neg2,op2);
-	    
+
 	    if (((op2==Opcode.EQ)&&(size1==size2))||
 		((op2==Opcode.NE)&&(size1!=size2))||
 		((op2==Opcode.GE)&&(size1>=size2))||
@@ -309,7 +446,7 @@ class AbstractInterferes {
 	    (dp.getPredicate() instanceof ExprPredicate)&&
 	    (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
 	    (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
-	    
+
 	    boolean neg1=ar.getPredicate().isNegated();
 	    Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
 	    boolean isInt1=((ExprPredicate)ar.getPredicate().getPredicate()).isRightInt();
@@ -323,7 +460,7 @@ class AbstractInterferes {
 	    int size2=isInt2?((ExprPredicate)dp.getPredicate()).rightSize():0;
 	    Expr expr2=((OpExpr)((ExprPredicate)dp.getPredicate()).expr).right;
 
-	    
+
 	    /* If the left sides of the comparisons are both from
                different sets, the update is orthogonal to the expr dp */
 	    {
@@ -338,7 +475,7 @@ class AbstractInterferes {
 	    /* Translate the opcodes */
 	    op1=Opcode.translateOpcode(neg1,op1);
 	    op2=Opcode.translateOpcode(neg2,op2);
-	    
+
 	    /* Obvious cases which can't interfere */
 	    if (((op1==Opcode.GT)||
 		(op1==Opcode.GE))&&
@@ -367,7 +504,7 @@ class AbstractInterferes {
 		    size1a--;
 		if (op1==Opcode.NE)
 		    size1a++; /*FLAGNE this is current behavior for NE repairs */
-		
+
 		if (op2==Opcode.GT)
 		    size2a++;
 		if (op2==Opcode.LT)
@@ -584,7 +721,7 @@ class AbstractInterferes {
 		    (op2==Opcode.LE)||
 		    (op2==Opcode.LT))
 		    return false;
-	    } 
+	    }
 	}
 	if ((des==dp.getPredicate().getDescriptor())&&
 	    satisfy&&
diff --git a/Repair/RepairCompiler/MCC/IR/Constraint.java b/Repair/RepairCompiler/MCC/IR/Constraint.java
index a506b03..c15d749 100755
--- a/Repair/RepairCompiler/MCC/IR/Constraint.java
+++ b/Repair/RepairCompiler/MCC/IR/Constraint.java
@@ -3,13 +3,13 @@ package MCC.IR;
 import java.util.*;
 
 public class Constraint implements Quantifiers {
-    
+
     private static int count = 1;
 
     String label = null;
     boolean crash = false;
     SymbolTable st = new SymbolTable();
-    Vector quantifiers = new Vector(); 
+    Vector quantifiers = new Vector();
     LogicStatement logicstatement = null;
     DNFConstraint dnfconstraint;
     int num;
@@ -19,6 +19,10 @@ public class Constraint implements Quantifiers {
         label = new String("c" + count++);
     }
 
+    public DNFConstraint getDNFConstraint() {
+        return dnfconstraint;
+    }
+
     public String toString() {
 	String name="";
 	for(int i=0;i<numQuantifiers();i++) {
@@ -61,7 +65,7 @@ public class Constraint implements Quantifiers {
     public LogicStatement getLogicStatement() {
         return logicstatement;
     }
-    
+
     public void setCrash(boolean crash) {
         this.crash = crash;
     }
@@ -74,7 +78,7 @@ public class Constraint implements Quantifiers {
 
         HashSet topdescriptors = new HashSet();
 
-        for (int i = 0; i < quantifiers.size(); i++) {            
+        for (int i = 0; i < quantifiers.size(); i++) {
             Quantifier q = (Quantifier) quantifiers.elementAt(i);
             topdescriptors.addAll(q.getRequiredDescriptors());
         }
@@ -83,18 +87,17 @@ public class Constraint implements Quantifiers {
     }
 
     public Set getRequiredDescriptorsFromLogicStatement() {
-        
+
         HashSet topdescriptors = new HashSet();
 
         topdescriptors.addAll(logicstatement.getRequiredDescriptors());
 
         return SetDescriptor.expand(topdescriptors);
     }
-   
+
     public Set getRequiredDescriptors() {
         Set set = getRequiredDescriptorsFromQuantifiers();
         set.addAll(getRequiredDescriptorsFromLogicStatement());
         return set;
     }
 }
-
diff --git a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
index 55770f5..72b73c4 100755
--- a/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
+++ b/Repair/RepairCompiler/MCC/IR/DNFConstraint.java
@@ -47,6 +47,16 @@ public class DNFConstraint {
 	return new DNFConstraint(vector);
     }
 
+    public DNFConstraint copyminus(Conjunction c) {
+	Vector vector=new Vector();
+	for (int i=0;i<size();i++) {
+           Conjunction cur_conj=get(i);
+           if (c!=cur_conj)
+              vector.add(cur_conj.copy());
+	}
+	return new DNFConstraint(vector);
+    }
+
     public DNFConstraint and(DNFConstraint c) {
 	DNFConstraint newdnf=new DNFConstraint();
 	for(int i=0;i<size();i++) {
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 09e1abe..ff9a293 100755
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -50,7 +50,7 @@ public class Termination {
 	predtoabstractmap=new Hashtable();
 	if (!Compiler.REPAIR)
 	    return;
-	
+
 
 	for(int i=0;i<state.vRules.size();i++)
 	    System.out.println(state.vRules.get(i));
@@ -129,14 +129,14 @@ public class Termination {
 	    DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
 	    HashSet superset=new HashSet();
 	    Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
-	    
+
 	    if (di.conjunctionnum==-1) {
 		superset.addAll((Set)conjunctionmap.get(constr));
 	    } else {
 		DNFConstraint dnf=constr.dnfconstraint;
 		superset.add(conjtonodemap.get(dnf.get(di.conjunctionnum)));
 	    }
-	    
+
 	    GraphNode.boundedcomputeclosure(superset,null,di.depth);
 	    try {
 		GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+(di.conjunctionnum==-1?"":"-"+di.conjunctionnum)+".dot"),superset);
@@ -251,7 +251,7 @@ public class Termination {
 	    }
 	    /* 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);  
+		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);
@@ -271,7 +271,7 @@ public class Termination {
 	    GraphNode gn=(GraphNode)absiterator.next();
 	    TermNode tn=(TermNode)gn.getOwner();
 	    AbstractRepair ar=(AbstractRepair)tn.getAbstract();
-	
+
 	    for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 		GraphNode gn2=(GraphNode)conjiterator.next();
 		TermNode tn2=(TermNode)gn2.getOwner();
@@ -279,19 +279,25 @@ public class Termination {
 		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.interferesquantifier(ar,cons)||
-			abstractinterferes.interfereswithpredicate(ar,dp)) {
-			GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
-			gn.addEdge(e);
-			break;
-		    }
-		}
+                if (AbstractInterferes.interferesquantifier(ar,cons)) {
+                    GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                    gn.addEdge(e);
+                } else {
+                    for(int i=0;i<conj.size();i++) {
+                        DNFPredicate dp=conj.get(i);
+                        if (getConstraint(gn)!=null&&
+                            abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons))
+                            continue;
+
+                        if (abstractinterferes.interfereswithpredicate(ar,dp)) {
+                            GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+                            gn.addEdge(e);
+                            break;
+                        }
+                    }
+                }
 	    }
 	    for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 		GraphNode gn2=(GraphNode)scopeiterator.next();
@@ -305,6 +311,18 @@ public class Termination {
 	}
     }
 
+    Constraint getConstraint(GraphNode gn) {
+        for(Iterator it=gn.inedges();it.hasNext();) {
+            GraphNode.Edge e=(GraphNode.Edge)it.next();
+            GraphNode gnsource=e.getSource();
+            TermNode tnsource=(TermNode)gnsource.getOwner();
+            if (tnsource.getType()==TermNode.CONJUNCTION) {
+                return tnsource.getConstraint();
+            }
+        }
+        return null;
+    }
+
     void generatescopenodes() {
 	for(int i=0;i<state.vRules.size();i++) {
 	    Rule r=(Rule) state.vRules.get(i);
@@ -335,13 +353,13 @@ public class Termination {
 	    scopenodes.add(gnfalsify);
 	}
     }
-    
+
     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();
@@ -445,7 +463,7 @@ public class Termination {
 	    abstractrepair.add(gn);
 	    abstractrepairadd.add(gn);
 	    abstractadd.put(sd,gn);
-	    
+
 	    DNFPredicate tp2=new DNFPredicate(true,ip);
 	    AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd,sources);
 	    TermNode tn2=new TermNode(ar2);
@@ -465,7 +483,7 @@ public class Termination {
 	    VarExpr ve2=new VarExpr("DUMMY2");
 
 	    InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
-	    
+
 	    DNFPredicate tp=new DNFPredicate(false,ip);
 	    AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd,sources);
 	    TermNode tn=new TermNode(ar);
@@ -476,7 +494,7 @@ public class Termination {
 	    abstractrepair.add(gn);
 	    abstractrepairadd.add(gn);
 	    abstractadd.put(rd,gn);
-	    
+
 	    DNFPredicate tp2=new DNFPredicate(true,ip);
 	    AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd,sources);
 	    TermNode tn2=new TermNode(ar2);
@@ -546,7 +564,7 @@ public class Termination {
 		}
 		if (!un.checkupdates()) /* Make sure we have a good update */
 		    continue;
-		
+
 		mun.addUpdate(un);
 		GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
 		compensationcount++;
@@ -601,7 +619,7 @@ public class Termination {
 	}
 	if (possiblerules.size()==0)
 	    return;
-	
+
 	/* Loop through different ways of falsifying each of these rules */
 	int[] count=new int[possiblerules.size()];
 	while(remains(count,possiblerules,true)) {
@@ -657,8 +675,7 @@ public class Termination {
 		mun.addUpdate(un);
 	    }
 	    if (goodflag) {
-		GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
-		removefromcount++;
+		GraphNode.Edge e=new GraphNode.Edge("abstract"+(removefromcount++),gn2);
 		gn.addEdge(e);
 		updatenodes.add(gn2);
 	    }
@@ -704,7 +721,7 @@ public class Termination {
 	int rightindex=1;
 	if (inverted)
 	    leftindex=2;
-	else 
+	else
 	    rightindex=2;
 
 	// construct set of possible rules
@@ -723,13 +740,13 @@ public class Termination {
 	while(remains(count,possiblerules,false)) {
 	    MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
 	    TermNode tn=new TermNode(mun);
-	    GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
+	    GraphNode gn2=new GraphNode("UpdateMod"+modifycount,tn);
 
 	    boolean goodflag=true;
 	    for(int i=0;i<possiblerules.size();i++) {
 		Rule r=(Rule)possiblerules.get(i);
 		UpdateNode un=new UpdateNode(r);
-		
+
 		int c=count[i];
 		if (!processconjunction(un,r.getDNFGuardExpr().get(c),null)) {
 		    goodflag=false;break;
@@ -767,10 +784,10 @@ public class Termination {
 		    if (vd.isGlobal()) {
 			Updates up=new Updates(ri.getRightExpr(),rightindex,null);
 			un.addUpdate(up);
-		    } else if (!inverted) 
+		    } else if (!inverted)
 			goodflag=false;
 		}
-				
+
 		if (!un.checkupdates()) {
 		    goodflag=false;
 		    break;
@@ -801,7 +818,7 @@ public class Termination {
 		 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 		(r.getInclusion() instanceof RelationInclusion&&
 		 ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
-		
+
 		/* First solve for quantifiers */
 		Vector bindings=new Vector();
 		/* Construct bindings */
@@ -823,7 +840,7 @@ public class Termination {
 		    if(inc instanceof SetInclusion) {
 			SetInclusion si=(SetInclusion)inc;
 			Expr e=si.elementexpr;
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=si.getSet().getType())
@@ -861,7 +878,7 @@ public class Termination {
 			RelationInclusion ri=(RelationInclusion)inc;
 
 			Expr e=ri.getLeftExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getDomain().getType())
@@ -902,9 +919,9 @@ public class Termination {
 				un.addUpdate(up);
 			    }
      			}
-			
+
 			e=ri.getRightExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getRange().getType())
@@ -926,7 +943,7 @@ public class Termination {
 				if (set==null)
 				    continue;
 				ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
-				
+
 				if (rap==ArrayAnalysis.AccessPath.NONE||
 				    !rap.equal(ap)||
 				    !constructarrayupdate(un, e, rap, 1))
@@ -982,7 +999,7 @@ public class Termination {
 	for (int i=ap.numFields()-1;i>=0;i--) {
 	    if (e==null)
 		e=lexpr;
-	    else 
+	    else
 		e=((DotExpr)e).getExpr();
 
 	    while (e instanceof CastExpr)
@@ -1035,7 +1052,7 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 			/* Can solve for v */
@@ -1059,7 +1076,7 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 				/* Can solve for v */
@@ -1080,7 +1097,7 @@ public class Termination {
 			    return false;
 			e=ce.getExpr();
 		    }
-		    
+
 		    if ((e instanceof VarExpr)&&
 			(((VarExpr)e).getVar()==vd)) {
 				/* Can solve for v */
@@ -1118,7 +1135,7 @@ public class Termination {
 			SetInclusion si=(SetInclusion)inc;
 
 			Expr e=si.elementexpr;
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=td)
@@ -1143,7 +1160,7 @@ public class Termination {
 
 
 			Expr e=ri.getLeftExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getDomain().getType())
@@ -1163,7 +1180,7 @@ public class Termination {
 
 
 			e=ri.getRightExpr();
-			
+
 			while(e instanceof CastExpr) {
 			    CastExpr ce=(CastExpr)e;
 			    if (ce.getType()!=ri.getRelation().getRange().getType())
@@ -1198,10 +1215,10 @@ public class Termination {
 	}
 	return goodupdate;
     }
-    
+
     /** Adds updates that add an item to the appropriate set or
      * relation quantified over by the model definition rule.. */
-    
+
     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r,Hashtable setmapping) {
 	Inclusion inc=r.getInclusion();
 	for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
@@ -1284,7 +1301,7 @@ public class Termination {
 	    } else if (e instanceof TupleOfExpr) {
 		Updates up=new Updates(e,de.getNegation());
 		un.addUpdate(up);
-	    } else if (e instanceof BooleanLiteralExpr) { 
+	    } else if (e instanceof BooleanLiteralExpr) {
 		boolean truth=((BooleanLiteralExpr)e).getValue();
 		if (de.getNegation())
 		    truth=!truth;
-- 
2.34.1