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