Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5
   6 public class Termination {
   7     HashSet conjunctions;
   8     Hashtable conjunctionmap;
   9
  10     HashSet abstractrepair;
  11     HashSet updatenodes;
  12     HashSet consequencenodes;
  13
  14     HashSet scopenodes;
  15     Hashtable scopesatisfy;
  16     Hashtable scopefalsify;
  17     Hashtable consequence;
  18     Hashtable abstractadd;
  19     Hashtable abstractremove;
  20
  21     State state;
  22
  23     public Termination(State state) {
  24         this.state=state;
  25         conjunctions=new HashSet();
  26         conjunctionmap=new Hashtable();
  27         abstractrepair=new HashSet();
  28         scopenodes=new HashSet();
  29         scopesatisfy=new Hashtable();
  30         scopefalsify=new Hashtable();
  31         consequence=new Hashtable();
  32         updatenodes=new HashSet();
  33         consequencenodes=new HashSet();
  34         abstractadd=new Hashtable();
  35         abstractremove=new Hashtable();
  36
  37
  38         generateconjunctionnodes();
  39         generatescopenodes();
  40         generaterepairnodes();
  41         generatedatastructureupdatenodes();
  42         generatecompensationnodes();
  43
  44         generateabstractedges();
  45         generatescopeedges();
  46         generateupdateedges();
  47
  48         HashSet superset=new HashSet();
  49         superset.addAll(conjunctions);
  50         //superset.addAll(abstractrepair);
  51         //superset.addAll(updatenodes);
  52         //superset.addAll(scopenodes);
  53         //superset.addAll(consequencenodes);
  54         GraphNode.computeclosure(superset,null);
  55         try {
  56             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
  57         } catch (Exception e) {
  58             e.printStackTrace();
  59             System.exit(-1);
  60         }
  61         for(Iterator it=updatenodes.iterator();it.hasNext();) {
  62             GraphNode gn=(GraphNode)it.next();
  63             TermNode tn=(TermNode)gn.getOwner();
  64             MultUpdateNode mun=tn.getUpdate();
  65             System.out.println(gn.getTextLabel());
  66             System.out.println(mun.toString());
  67         }
  68         GraphAnalysis ga=new GraphAnalysis(this);
  69         Set toremove=ga.doAnalysis();
  70         System.out.println("Removing:");
  71         for(Iterator it=toremove.iterator();it.hasNext();) {
  72             GraphNode gn=(GraphNode)it.next();
  73             System.out.println(gn.getTextLabel());
  74         }
  75     }
  76
  77     void generateconjunctionnodes() {
  78         Vector constraints=state.vConstraints;
  79         for(int i=0;i<constraints.size();i++) {
  80             Constraint c=(Constraint)constraints.get(i);
  81             DNFConstraint dnf=c.dnfconstraint;
  82             for(int j=0;j<dnf.size();j++) {
  83                 TermNode tn=new TermNode(c,dnf.get(j));
  84                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
  85                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
  86                                            ,tn);
  87                 conjunctions.add(gn);
  88                 if (!conjunctionmap.containsKey(c))
  89                     conjunctionmap.put(c,new HashSet());
  90                 ((Set)conjunctionmap.get(c)).add(gn);
  91             }
  92         }
  93     }
  94
  95     void generateupdateedges() {
  96         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
  97             GraphNode gn=(GraphNode)updateiterator.next();
  98             TermNode tn=(TermNode)gn.getOwner();
  99             MultUpdateNode mun=tn.getUpdate();
 100             /* Cycle through the rules to look for possible conflicts */
 101             for(int i=0;i<state.vRules.size();i++) {
 102                 Rule r=(Rule) state.vRules.get(i);
 103                 if (ConcreteInterferes.interferes(mun,r,true)) {
 104                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 105                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 106                     gn.addEdge(e);
 107                 }
 108                 if (ConcreteInterferes.interferes(mun,r,false)) {
 109                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 110                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 111                     gn.addEdge(e);
 112                 }
 113             }
 114         }
 115     }
 116
 117     void generateabstractedges() {
 118         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 119             GraphNode gn=(GraphNode)absiterator.next();
 120             TermNode tn=(TermNode)gn.getOwner();
 121             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
 122
 123             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 124                 GraphNode gn2=(GraphNode)conjiterator.next();
 125                 TermNode tn2=(TermNode)gn2.getOwner();
 126                 Conjunction conj=tn2.getConjunction();
 127                 Constraint cons=tn2.getConstraint();
 128
 129                 for(int i=0;i<conj.size();i++) {
 130                     DNFPredicate dp=conj.get(i);
 131                     if (AbstractInterferes.interferes(ar,cons)||
 132                         AbstractInterferes.interferes(ar,dp)) {
 133                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 134                         gn.addEdge(e);
 135                         break;
 136                     }
 137                 }
 138             }
 139
 140             for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 141                 GraphNode gn2=(GraphNode)scopeiterator.next();
 142                 TermNode tn2=(TermNode)gn2.getOwner();
 143                 ScopeNode sn2=tn2.getScope();
 144                 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
 145                     GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 146                     gn.addEdge(e);
 147                 }
 148             }
 149         }
 150     }
 151
 152     void generatescopeedges() {
 153         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 154             GraphNode gn=(GraphNode)scopeiterator.next();
 155             TermNode tn=(TermNode)gn.getOwner();
 156             ScopeNode sn=tn.getScope();
 157
 158             /* Interference edges with conjunctions */
 159             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 160                 GraphNode gn2=(GraphNode)conjiterator.next();
 161                 TermNode tn2=(TermNode)gn2.getOwner();
 162                 Conjunction conj=tn2.getConjunction();
 163                 Constraint constr=tn2.getConstraint();
 164                 for(int i=0;i<conj.size();i++) {
 165                     DNFPredicate dp=conj.get(i);
 166                     if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
 167                         AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 168                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 169                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 170                         gnconseq.addEdge(e);
 171                         break;
 172                     }
 173                 }
 174             }
 175
 176             /* Now see if this could effect other model defintion rules */
 177             for(int i=0;i<state.vRules.size();i++) {
 178                 Rule r=(Rule) state.vRules.get(i);
 179                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 180                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 181                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 182                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 183                     gnconseq.addEdge(e);
 184                 }
 185                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 186                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 187                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 188                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 189                     gnconseq.addEdge(e);
 190                 }
 191             }
 192         }
 193     }
 194
 195     /* Generates the abstract repair nodes */
 196     void generaterepairnodes() {
 197         /* Generate repairs of conjunctions */
 198         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 199             GraphNode gn=(GraphNode)conjiterator.next();
 200             TermNode tn=(TermNode)gn.getOwner();
 201             Conjunction conj=tn.getConjunction();
 202             for(int i=0;i<conj.size();i++) {
 203                 DNFPredicate dp=conj.get(i);
 204                 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
 205                 Descriptor d=dp.getPredicate().getDescriptor();
 206                 for(int j=0;j<array.length;j++) {
 207                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
 208                     TermNode tn2=new TermNode(ar);
 209                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
 210                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 211                     gn.addEdge(e);
 212                     abstractrepair.add(gn2);
 213                 }
 214             }
 215         }
 216         /* Generate additional abstract repairs */
 217         Vector setdescriptors=state.stSets.getAllDescriptors();
 218         for(int i=0;i<setdescriptors.size();i++) {
 219             SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
 220
 221             /* XXXXXXX: Not sure what to do here */
 222             VarExpr ve=new VarExpr("DUMMY");
 223             InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
 224
 225             DNFPredicate tp=new DNFPredicate(false,ip);
 226             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
 227             TermNode tn=new TermNode(ar);
 228             GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
 229             abstractrepair.add(gn);
 230             abstractadd.put(sd,gn);
 231
 232             DNFPredicate tp2=new DNFPredicate(true,ip);
 233             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
 234             TermNode tn2=new TermNode(ar2);
 235             GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
 236             abstractrepair.add(gn2);
 237             abstractremove.put(sd,gn2);
 238         }
 239
 240         Vector relationdescriptors=state.stRelations.getAllDescriptors();
 241         for(int i=0;i<relationdescriptors.size();i++) {
 242             RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
 243
 244             /* XXXXXXX: Not sure what to do here */
 245             VarDescriptor vd1=new VarDescriptor("DUMMY1");
 246             VarExpr ve2=new VarExpr("DUMMY2");
 247
 248             InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
 249
 250             DNFPredicate tp=new DNFPredicate(false,ip);
 251             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
 252             TermNode tn=new TermNode(ar);
 253             GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
 254             abstractrepair.add(gn);
 255             abstractadd.put(rd,gn);
 256
 257             DNFPredicate tp2=new DNFPredicate(true,ip);
 258             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
 259             TermNode tn2=new TermNode(ar2);
 260             GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
 261             abstractrepair.add(gn2);
 262             abstractremove.put(rd,gn2);
 263         }
 264
 265     }
 266
 267     int compensationcount=0;
 268     void generatecompensationnodes() {
 269         for(int i=0;i<state.vRules.size();i++) {
 270             Rule r=(Rule) state.vRules.get(i);
 271             Vector possiblerules=new Vector();
 272             /* Construct bindings */
 273             Vector bindings=new Vector();
 274             constructbindings(bindings, r,true);
 275
 276             for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
 277                 GraphNode gn=(GraphNode)scopesatisfy.get(r);
 278                 TermNode tn=(TermNode) gn.getOwner();
 279                 ScopeNode sn=tn.getScope();
 280                 MultUpdateNode mun=new MultUpdateNode(sn);
 281                 TermNode tn2=new TermNode(mun);
 282                 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
 283                 UpdateNode un=new UpdateNode(r);
 284                 un.addBindings(bindings);
 285                 if (j<r.numQuantifiers()) {
 286                     /* Remove quantifier */
 287                     Quantifier q=r.getQuantifier(j);
 288                     if (q instanceof RelationQuantifier) {
 289                         RelationQuantifier rq=(RelationQuantifier)q;
 290                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 291                         toe.td=ReservedTypeDescriptor.INT;
 292                         Updates u=new Updates(toe,true);
 293                         un.addUpdate(u);
 294                         if (abstractremove.containsKey(rq.relation)) {
 295                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 296                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 297                             gn2.addEdge(e);
 298                         } else {
 299                             continue; /* Abstract repair doesn't exist */
 300                         }
 301                     } else if (q instanceof SetQuantifier) {
 302                         SetQuantifier sq=(SetQuantifier)q;
 303                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 304                         eoe.td=ReservedTypeDescriptor.INT;
 305                         Updates u=new Updates(eoe,true);
 306                         un.addUpdate(u);
 307                         if (abstractremove.containsKey(sq.set)) {
 308                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 309                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 310                             gn2.addEdge(e);
 311                         } else {
 312                             continue; /* Abstract repair doesn't exist */
 313                         }
 314                     } else {
 315                         continue;
 316                     }
 317                 } else {
 318                     int c=j-r.numQuantifiers();
 319                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 320                         continue;
 321                     }
 322                 }
 323                 if (!un.checkupdates()) /* Make sure we have a good update */
 324                     continue;
 325
 326                 mun.addUpdate(un);
 327
 328                 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
 329                 compensationcount++;
 330                 gn.addEdge(e);
 331                 updatenodes.add(gn2);
 332             }
 333         }
 334     }
 335
 336     void generatedatastructureupdatenodes() {
 337         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 338             GraphNode gn=(GraphNode)absiterator.next();
 339             TermNode tn=(TermNode) gn.getOwner();
 340             AbstractRepair ar=tn.getAbstract();
 341             if (ar.getType()==AbstractRepair.ADDTOSET) {
 342                 generateaddtosetrelation(gn,ar);
 343             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 344                 generateremovefromsetrelation(gn,ar);
 345             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 346                 generateaddtosetrelation(gn,ar);
 347             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 348                 generateremovefromsetrelation(gn,ar);
 349             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 350                 /* Generate remove/add pairs */
 351                 generateremovefromsetrelation(gn,ar);
 352                 generateaddtosetrelation(gn,ar);
 353                 /* Generate atomic modify */
 354                 generatemodifyrelation(gn,ar);
 355             }
 356         }
 357     }
 358
 359     int removefromcount=0;
 360     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
 361         Vector possiblerules=new Vector();
 362         for(int i=0;i<state.vRules.size();i++) {
 363             Rule r=(Rule) state.vRules.get(i);
 364             if ((r.getInclusion() instanceof SetInclusion)&&
 365                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 366                 possiblerules.add(r);
 367             if ((r.getInclusion() instanceof RelationInclusion)&&
 368                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
 369                 possiblerules.add(r);
 370         }
 371         if (possiblerules.size()==0)
 372             return;
 373         int[] count=new int[possiblerules.size()];
 374         while(remains(count,possiblerules)) {
 375             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
 376             TermNode tn=new TermNode(mun);
 377             GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 378
 379             boolean goodflag=true;
 380             for(int i=0;i<possiblerules.size();i++) {
 381                 Rule r=(Rule)possiblerules.get(i);
 382                 UpdateNode un=new UpdateNode(r);
 383                 /* Construct bindings */
 384                 Vector bindings=new Vector();
 385                 constructbindings(bindings, r,true);
 386                 un.addBindings(bindings);
 387                 if (count[i]<r.numQuantifiers()) {
 388                     /* Remove quantifier */
 389                     Quantifier q=r.getQuantifier(count[i]);
 390                     if (q instanceof RelationQuantifier) {
 391                         RelationQuantifier rq=(RelationQuantifier)q;
 392                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 393                         toe.td=ReservedTypeDescriptor.INT;
 394                         Updates u=new Updates(toe,true);
 395                         un.addUpdate(u);
 396                         if (abstractremove.containsKey(rq.relation)) {
 397                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 398                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 399                             gn2.addEdge(e);
 400                         } else {
 401                             goodflag=false;break; /* Abstract repair doesn't exist */
 402                         }
 403                     } else if (q instanceof SetQuantifier) {
 404                         SetQuantifier sq=(SetQuantifier)q;
 405                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 406                         eoe.td=ReservedTypeDescriptor.INT;
 407                         Updates u=new Updates(eoe,true);
 408                         un.addUpdate(u);
 409                         if (abstractremove.containsKey(sq.set)) {
 410                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 411                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 412                             gn2.addEdge(e);
 413                         } else {
 414                             goodflag=false;break; /* Abstract repair doesn't exist */
 415                         }
 416                     } else {goodflag=false;break;}
 417                 } else {
 418                     int c=count[i]-r.numQuantifiers();
 419                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 420                         goodflag=false;break;
 421                     }
 422                 }
 423                 if (!un.checkupdates()) {
 424                     goodflag=false;
 425                     break;
 426                 }
 427                 mun.addUpdate(un);
 428             }
 429             if (goodflag) {
 430                 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
 431                 removefromcount++;
 432                 gn.addEdge(e);
 433                 updatenodes.add(gn2);
 434             }
 435             increment(count,possiblerules);
 436         }
 437     }
 438
 439     static void increment(int count[], Vector rules) {
 440         count[0]++;
 441         for(int i=0;i<(rules.size()-1);i++) {
 442             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 443                 count[i+1]++;
 444                 count[i]=0;
 445             } else break;
 446         }
 447     }
 448
 449     static boolean remains(int count[], Vector rules) {
 450         for(int i=0;i<rules.size();i++) {
 451             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 452                 return false;
 453             }
 454         }
 455         return true;
 456     }
 457
 458     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
 459     }
 460
 461
 462     boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
 463         boolean goodupdate=true;
 464         Inclusion inc=r.getInclusion();
 465         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 466             Quantifier q=(Quantifier)iterator.next();
 467             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 468                 VarDescriptor vd=null;
 469                 SetDescriptor set=null;
 470                 if (q instanceof SetQuantifier) {
 471                     vd=((SetQuantifier)q).getVar();
 472                 } else
 473                     vd=((ForQuantifier)q).getVar();
 474                 if(inc instanceof SetInclusion) {
 475                     SetInclusion si=(SetInclusion)inc;
 476                     if ((si.elementexpr instanceof VarExpr)&&
 477                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 478                         /* Can solve for v */
 479                         Binding binding=new Binding(vd,0);
 480                         bindings.add(binding);
 481                     } else
 482                         goodupdate=false;
 483                 } else if (inc instanceof RelationInclusion) {
 484                     RelationInclusion ri=(RelationInclusion)inc;
 485                     boolean f1=true;
 486                     boolean f2=true;
 487                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 488                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 489                                 /* Can solve for v */
 490                         Binding binding=new Binding(vd,0);
 491                         bindings.add(binding);
 492                     } else f1=false;
 493                     if ((ri.getRightExpr() instanceof VarExpr)&&
 494                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 495                                 /* Can solve for v */
 496                         Binding binding=new Binding(vd,0);
 497                         bindings.add(binding);
 498                     } else f2=false;
 499                     if (!(f1||f2))
 500                         goodupdate=false;
 501                 } else throw new Error("Inclusion not recognized");
 502                 if (!goodupdate)
 503                     if (isremoval) {
 504                         Binding binding=new Binding(vd);
 505                         bindings.add(binding);
 506                         goodupdate=true;
 507                     } else
 508                         break;
 509             } else if (q instanceof RelationQuantifier) {
 510                 RelationQuantifier rq=(RelationQuantifier)q;
 511                 for(int k=0;k<2;k++) {
 512                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 513                     if(inc instanceof SetInclusion) {
 514                         SetInclusion si=(SetInclusion)inc;
 515                         if ((si.elementexpr instanceof VarExpr)&&
 516                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 517                             /* Can solve for v */
 518                             Binding binding=new Binding(vd,0);
 519                             bindings.add(binding);
 520                         } else
 521                             goodupdate=false;
 522                     } else if (inc instanceof RelationInclusion) {
 523                         RelationInclusion ri=(RelationInclusion)inc;
 524                         boolean f1=true;
 525                         boolean f2=true;
 526                         if ((ri.getLeftExpr() instanceof VarExpr)&&
 527                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 528                             /* Can solve for v */
 529                             Binding binding=new Binding(vd,0);
 530                             bindings.add(binding);
 531                         } else f1=false;
 532                         if ((ri.getRightExpr() instanceof VarExpr)&&
 533                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 534                             /* Can solve for v */
 535                             Binding binding=new Binding(vd,0);
 536                             bindings.add(binding);
 537                         } else f2=false;
 538                         if (!(f1||f2))
 539                             goodupdate=false;
 540                     } else throw new Error("Inclusion not recognized");
 541                     if (!goodupdate)
 542                         if (isremoval) {
 543                             Binding binding=new Binding(vd);
 544                             bindings.add(binding);
 545                             goodupdate=true;
 546                         } else
 547                             break;
 548                 }
 549                 if (!goodupdate)
 550                     break;
 551             } else throw new Error("Quantifier not recognized");
 552         }
 553         return goodupdate;
 554     }
 555
 556     static int addtocount=0;
 557     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
 558         //      System.out.println("Attempting to generate add to set");
 559         //System.out.println(ar.getPredicate().getPredicate().name());
 560         //System.out.println(ar.getPredicate().isNegated());
 561         for(int i=0;i<state.vRules.size();i++) {
 562             Rule r=(Rule) state.vRules.get(i);
 563             /* See if this is a good rule*/
 564             //System.out.println(r.getGuardExpr().name());
 565             if ((r.getInclusion() instanceof SetInclusion&&
 566                 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 567                 (r.getInclusion() instanceof RelationInclusion&&
 568                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 569
 570                 /* First solve for quantifiers */
 571                 Vector bindings=new Vector();
 572                 /* Construct bindings */
 573                 //System.out.println("Attempting to generate add to set: #2");
 574                 if (!constructbindings(bindings,r,false))
 575                     continue;
 576                 //System.out.println("Attempting to generate add to set: #3");
 577                 //Generate add instruction
 578                 DNFRule dnfrule=r.getDNFGuardExpr();
 579                 for(int j=0;j<dnfrule.size();j++) {
 580                     Inclusion inc=r.getInclusion();
 581                     UpdateNode un=new UpdateNode(r);
 582                     un.addBindings(bindings);
 583                     /* Now build update for tuple/set inclusion condition */
 584                     if(inc instanceof SetInclusion) {
 585                         SetInclusion si=(SetInclusion)inc;
 586                         if (!(si.elementexpr instanceof VarExpr)) {
 587                             Updates up=new Updates(si.elementexpr,0);
 588                             un.addUpdate(up);
 589                         } else {
 590                             VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 591                             if (un.getBinding(vd)==null) {
 592                                 Updates up=new Updates(si.elementexpr,0);
 593                                 un.addUpdate(up);
 594                             }
 595                         }
 596                     } else if (inc instanceof RelationInclusion) {
 597                         RelationInclusion ri=(RelationInclusion)inc;
 598                         if (!(ri.getLeftExpr() instanceof VarExpr)) {
 599                             Updates up=new Updates(ri.getLeftExpr(),0);
 600                             un.addUpdate(up);
 601                         } else {
 602                             VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 603                             if (un.getBinding(vd)==null) {
 604                                 Updates up=new Updates(ri.getLeftExpr(),0);
 605                                 un.addUpdate(up);
 606                             }
 607                         }
 608                         if (!(ri.getRightExpr() instanceof VarExpr)) {
 609                             Updates up=new Updates(ri.getRightExpr(),1);
 610                             un.addUpdate(up);
 611                         } else {
 612                             VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 613                             if (un.getBinding(vd)==null) {
 614                                 Updates up=new Updates(ri.getRightExpr(),1);
 615                                 un.addUpdate(up);
 616                             }
 617                         }
 618                     }
 619                     //Finally build necessary updates to satisfy conjunction
 620                     RuleConjunction ruleconj=dnfrule.get(j);
 621                     /* Add in updates for quantifiers */
 622                     //System.out.println("Attempting to generate add to set #4");
 623                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
 624                     TermNode tn=new TermNode(mun);
 625                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 626
 627                     if (processquantifers(gn2,un, r)&&debugdd()&&
 628                         processconjunction(un,ruleconj)&&
 629                         un.checkupdates()) {
 630                         //System.out.println("Attempting to generate add to set #5");
 631                         mun.addUpdate(un);
 632                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 633                         addtocount++;
 634                         gn.addEdge(e);
 635                         updatenodes.add(gn2);}
 636                 }
 637             }
 638         }
 639     }
 640
 641     boolean debugdd() {
 642         //System.out.println("Attempting to generate add to set DD");
 643         return true;
 644     }
 645
 646     boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
 647         Inclusion inc=r.getInclusion();
 648         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 649             Quantifier q=(Quantifier)iterator.next();
 650             /* Add quantifier */
 651             /* FIXME: Analysis to determine when this update is necessary */
 652             if (q instanceof RelationQuantifier) {
 653                 RelationQuantifier rq=(RelationQuantifier)q;
 654                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 655                 toe.td=ReservedTypeDescriptor.INT;
 656                 Updates u=new Updates(toe,false);
 657                 un.addUpdate(u);
 658                 if (abstractremove.containsKey(rq.relation)) {
 659                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
 660                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 661                     gn.addEdge(e);
 662                 } else {
 663                     return false;
 664                 }
 665
 666             } else if (q instanceof SetQuantifier) {
 667                 SetQuantifier sq=(SetQuantifier)q;
 668                 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 669                 eoe.td=ReservedTypeDescriptor.INT;
 670                 Updates u=new Updates(eoe,false);
 671                 un.addUpdate(u);
 672                 if (abstractremove.containsKey(sq.set)) {
 673                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
 674                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 675                     gn.addEdge(e);
 676                 } else {
 677                     return false;
 678                 }
 679             } else return false;
 680         }
 681         return true;
 682     }
 683
 684     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
 685         boolean okay=true;
 686         for(int k=0;k<ruleconj.size();k++) {
 687             DNFExpr de=ruleconj.get(k);
 688             Expr e=de.getExpr();
 689             if (e instanceof OpExpr) {
 690                 OpExpr ex=(OpExpr)de.getExpr();
 691                 Opcode op=ex.getOpcode();
 692                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
 693                 un.addUpdate(up);
 694             } else if (e instanceof ElementOfExpr) {
 695                 Updates up=new Updates(e,de.getNegation());
 696                 un.addUpdate(up);
 697             } else if (e instanceof TupleOfExpr) {
 698                 Updates up=new Updates(e,de.getNegation());
 699                 un.addUpdate(up);
 700             } else if (e instanceof BooleanLiteralExpr) {
 701                 boolean truth=((BooleanLiteralExpr)e).getValue();
 702                 if (de.getNegation())
 703                     truth=!truth;
 704                 if (!truth) {
 705                     okay=false;
 706                     break;
 707                 }
 708             } else {
 709                 System.out.println(e.getClass().getName());
 710                 throw new Error("Error #213");
 711             }
 712         }
 713         return okay;
 714     }
 715
 716     void generatescopenodes() {
 717         for(int i=0;i<state.vRules.size();i++) {
 718             Rule r=(Rule) state.vRules.get(i);
 719             ScopeNode satisfy=new ScopeNode(r,true);
 720             TermNode tnsatisfy=new TermNode(satisfy);
 721             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 722             ConsequenceNode cnsatisfy=new ConsequenceNode();
 723             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 724             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 725             consequence.put(satisfy,cgnsatisfy);
 726             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 727             gnsatisfy.addEdge(esat);
 728             consequencenodes.add(cgnsatisfy);
 729             scopesatisfy.put(r,gnsatisfy);
 730             scopenodes.add(gnsatisfy);
 731
 732             ScopeNode falsify=new ScopeNode(r,false);
 733             TermNode tnfalsify=new TermNode(falsify);
 734             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 735             ConsequenceNode cnfalsify=new ConsequenceNode();
 736             TermNode ctnfalsify=new TermNode(cnfalsify);
 737             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 738             consequence.put(falsify,cgnfalsify);
 739             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 740             gnfalsify.addEdge(efals);
 741             consequencenodes.add(cgnfalsify);
 742             scopefalsify.put(r,gnfalsify);
 743             scopenodes.add(gnfalsify);
 744         }
 745     }
 746 }