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