Improved termination analysis so that daikon generated specifications won't have...
authorbdemsky <bdemsky>
Mon, 8 Nov 2004 01:48:32 +0000 (01:48 +0000)
committerbdemsky <bdemsky>
Mon, 8 Nov 2004 01:48:32 +0000 (01:48 +0000)
Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
Repair/RepairCompiler/MCC/IR/Constraint.java
Repair/RepairCompiler/MCC/IR/DNFConstraint.java
Repair/RepairCompiler/MCC/IR/Termination.java

index 68ed221..df03933 100755 (executable)
@@ -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&&
index a506b03..c15d749 100755 (executable)
@@ -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;
     }
 }
-
index 55770f5..72b73c4 100755 (executable)
@@ -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++) {
index 09e1abe..ff9a293 100755 (executable)
@@ -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;