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