Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5 import MCC.Compiler;
   6
   7 public class Termination {
   8     HashSet conjunctions;
   9     Hashtable conjunctionmap;
  10
  11     HashSet abstractrepair;
  12     HashSet abstractrepairadd;
  13
  14     HashSet updatenodes;
  15     HashSet consequencenodes;
  16
  17     HashSet scopenodes;
  18     Hashtable scopesatisfy;
  19     Hashtable scopefalsify;
  20     Hashtable consequence;
  21     Hashtable abstractadd;
  22     Hashtable abstractremove;
  23     Hashtable conjtonodemap;
  24     Hashtable predtoabstractmap;
  25     Set removedset;
  26     ComputeMaxSize maxsize;
  27     State state;
  28     AbstractInterferes abstractinterferes;
  29     ConstraintDependence constraintdependence;
  30     ExactSize exactsize;
  31
  32     public Termination(State state) {
  33         this.state=state;
  34         conjunctions=new HashSet();
  35         conjunctionmap=new Hashtable();
  36         abstractrepair=new HashSet();
  37         abstractrepairadd=new HashSet();
  38         scopenodes=new HashSet();
  39         scopesatisfy=new Hashtable();
  40         scopefalsify=new Hashtable();
  41         consequence=new Hashtable();
  42         updatenodes=new HashSet();
  43         consequencenodes=new HashSet();
  44         abstractadd=new Hashtable();
  45         abstractremove=new Hashtable();
  46         conjtonodemap=new Hashtable();
  47         predtoabstractmap=new Hashtable();
  48         if (!Compiler.REPAIR)
  49             return;
  50
  51
  52         for(int i=0;i<state.vRules.size();i++)
  53             System.out.println(state.vRules.get(i));
  54         for(int i=0;i<state.vConstraints.size();i++)
  55             System.out.println(state.vConstraints.get(i));
  56
  57         maxsize=new ComputeMaxSize(state);
  58         exactsize=new ExactSize(state);
  59
  60         abstractinterferes=new AbstractInterferes(this);
  61         generateconjunctionnodes();
  62         constraintdependence=new ConstraintDependence(state,this);
  63
  64         generatescopenodes();
  65         generaterepairnodes();
  66         generatedatastructureupdatenodes();
  67         generatecompensationnodes();
  68
  69         generateabstractedges();
  70         generatescopeedges();
  71         generateupdateedges();
  72
  73
  74         HashSet superset=new HashSet();
  75         superset.addAll(conjunctions);
  76         HashSet closureset=new HashSet();
  77
  78         GraphNode.computeclosure(superset,closureset);
  79         try {
  80             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
  81         } catch (Exception e) {
  82             e.printStackTrace();
  83             System.exit(-1);
  84         }
  85         for(Iterator it=updatenodes.iterator();it.hasNext();) {
  86             GraphNode gn=(GraphNode)it.next();
  87             TermNode tn=(TermNode)gn.getOwner();
  88             MultUpdateNode mun=tn.getUpdate();
  89             System.out.println(gn.getTextLabel());
  90             System.out.println(mun.toString());
  91         }
  92         GraphAnalysis ga=new GraphAnalysis(this);
  93         removedset=ga.doAnalysis();
  94         if (removedset==null) {
  95             System.out.println("Can't generate terminating repair algorithm!");
  96             System.exit(-1);
  97         }
  98         constraintdependence.traversedependences(this);
  99
 100         System.out.println("Removing:");
 101         for(Iterator it=removedset.iterator();it.hasNext();) {
 102             GraphNode gn=(GraphNode)it.next();
 103             System.out.println(gn.getTextLabel());
 104         }
 105
 106         superset=new HashSet();
 107         superset.addAll(conjunctions);
 108         superset.removeAll(removedset);
 109         GraphNode.computeclosure(superset,removedset);
 110         try {
 111             GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
 112         } catch (Exception e) {
 113             e.printStackTrace();
 114             System.exit(-1);
 115         }
 116
 117     }
 118
 119
 120     /** This method generates a node for each conjunction in the DNF form of each constraint.
 121      * It also converts the quantifiers into conjunctions also - constraints can be satisfied by
 122      * removing items from the sets and relations they are quantified over */
 123     void generateconjunctionnodes() {
 124         Vector constraints=state.vConstraints;
 125         // Constructs conjunction nodes
 126         for(int i=0;i<constraints.size();i++) {
 127             Constraint c=(Constraint)constraints.get(i);
 128             DNFConstraint dnf=c.dnfconstraint;
 129             for(int j=0;j<dnf.size();j++) {
 130                 TermNode tn=new TermNode(c,dnf.get(j));
 131                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
 132                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
 133                                            ,tn);
 134                 conjunctions.add(gn);
 135                 if (!conjunctionmap.containsKey(c))
 136                     conjunctionmap.put(c,new HashSet());
 137                 ((Set)conjunctionmap.get(c)).add(gn);
 138                 conjtonodemap.put(dnf.get(j),gn);
 139
 140
 141             }
 142             // Construct quantifier "conjunction" nodes
 143             for(int j=0;j<c.numQuantifiers();j++) {
 144                 Quantifier q=c.getQuantifier(j);
 145                 if (q instanceof SetQuantifier) {
 146                     SetQuantifier sq=(SetQuantifier)q;
 147                     VarExpr ve=new VarExpr(sq.getVar());
 148                     InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
 149                     DNFConstraint dconst=new DNFConstraint(ip);
 150                     dconst=dconst.not();
 151                     TermNode tn=new TermNode(c,dconst.get(0));
 152                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 153                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 154                                                ,tn);
 155                     conjunctions.add(gn);
 156                     if (!conjunctionmap.containsKey(c))
 157                         conjunctionmap.put(c,new HashSet());
 158                     ((Set)conjunctionmap.get(c)).add(gn);
 159                     conjtonodemap.put(dconst.get(0),gn);
 160
 161                 } else if (q instanceof RelationQuantifier) {
 162                     RelationQuantifier rq=(RelationQuantifier)q;
 163                     VarExpr ve=new VarExpr(rq.y);
 164                     InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
 165                     DNFConstraint dconst=new DNFConstraint(ip);
 166                     dconst=dconst.not();
 167                     TermNode tn=new TermNode(c,dconst.get(0));
 168                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 169                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 170                                                ,tn);
 171                     conjunctions.add(gn);
 172                     if (!conjunctionmap.containsKey(c))
 173                         conjunctionmap.put(c,new HashSet());
 174                     ((Set)conjunctionmap.get(c)).add(gn);
 175                     conjtonodemap.put(dconst.get(0),gn);
 176
 177                 }
 178             }
 179         }
 180     }
 181
 182     void generateupdateedges() {
 183         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
 184             GraphNode gn=(GraphNode)updateiterator.next();
 185             TermNode tn=(TermNode)gn.getOwner();
 186             MultUpdateNode mun=tn.getUpdate();
 187             /* Cycle through the rules to look for possible conflicts */
 188             for(int i=0;i<state.vRules.size();i++) {
 189                 Rule r=(Rule) state.vRules.get(i);
 190                 if (ConcreteInterferes.interferes(mun,r,true)) {
 191                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 192                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 193                     gn.addEdge(e);
 194                 }
 195                 if (ConcreteInterferes.interferes(mun,r,false)) {
 196                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 197                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 198                     gn.addEdge(e);
 199                 }
 200             }
 201         }
 202     }
 203
 204     void generateabstractedges() {
 205         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 206             GraphNode gn=(GraphNode)absiterator.next();
 207             TermNode tn=(TermNode)gn.getOwner();
 208             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
 209
 210             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 211                 GraphNode gn2=(GraphNode)conjiterator.next();
 212                 TermNode tn2=(TermNode)gn2.getOwner();
 213                 Conjunction conj=tn2.getConjunction();
 214                 Constraint cons=tn2.getConstraint();
 215
 216                 for(int i=0;i<conj.size();i++) {
 217                     DNFPredicate dp=conj.get(i);
 218                     if (AbstractInterferes.interferes(ar,cons)||
 219                         abstractinterferes.interferes(ar,dp)) {
 220                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 221                         gn.addEdge(e);
 222                         break;
 223                     }
 224                 }
 225             }
 226
 227             for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 228                 GraphNode gn2=(GraphNode)scopeiterator.next();
 229                 TermNode tn2=(TermNode)gn2.getOwner();
 230                 ScopeNode sn2=tn2.getScope();
 231                 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
 232                     GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 233                     gn.addEdge(e);
 234                 }
 235             }
 236         }
 237     }
 238
 239     void generatescopeedges() {
 240         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 241             GraphNode gn=(GraphNode)scopeiterator.next();
 242             TermNode tn=(TermNode)gn.getOwner();
 243             ScopeNode sn=tn.getScope();
 244
 245             /* Interference edges with conjunctions */
 246             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 247                 GraphNode gn2=(GraphNode)conjiterator.next();
 248                 TermNode tn2=(TermNode)gn2.getOwner();
 249                 Conjunction conj=tn2.getConjunction();
 250                 Constraint constr=tn2.getConstraint();
 251                 for(int i=0;i<conj.size();i++) {
 252                     DNFPredicate dp=conj.get(i);
 253                     if (abstractinterferes.interferes(sn,dp)||
 254                         AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 255                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 256                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 257                         gnconseq.addEdge(e);
 258                         break;
 259                     }
 260                 }
 261             }
 262
 263             /* Now see if this could effect other model defintion rules */
 264             for(int i=0;i<state.vRules.size();i++) {
 265                 Rule r=(Rule) state.vRules.get(i);
 266                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 267                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 268                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 269                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 270                     gnconseq.addEdge(e);
 271                 }
 272                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 273                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 274                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 275                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 276                     gnconseq.addEdge(e);
 277                 }
 278             }
 279         }
 280     }
 281
 282     /** This method generates the abstract repair nodes. */
 283     void generaterepairnodes() {
 284         /* Generate repairs of conjunctions */
 285         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 286             GraphNode gn=(GraphNode)conjiterator.next();
 287             TermNode tn=(TermNode)gn.getOwner();
 288             Conjunction conj=tn.getConjunction();
 289             for(int i=0;i<conj.size();i++) {
 290                 DNFPredicate dp=conj.get(i);
 291                 int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
 292                 Descriptor d=dp.getPredicate().getDescriptor();
 293                 for(int j=0;j<array.length;j++) {
 294                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
 295                     TermNode tn2=new TermNode(ar);
 296                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
 297                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 298                     gn.addEdge(e);
 299                     if (!predtoabstractmap.containsKey(dp))
 300                         predtoabstractmap.put(dp,new HashSet());
 301                     ((Set)predtoabstractmap.get(dp)).add(gn2);
 302                     abstractrepair.add(gn2);
 303                 }
 304             }
 305         }
 306         /* Generate additional abstract repairs */
 307         Vector setdescriptors=state.stSets.getAllDescriptors();
 308         for(int i=0;i<setdescriptors.size();i++) {
 309             SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
 310
 311             /* XXXXXXX: Not sure what to do here */
 312             VarExpr ve=new VarExpr("DUMMY");
 313             InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
 314
 315             DNFPredicate tp=new DNFPredicate(false,ip);
 316             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
 317             TermNode tn=new TermNode(ar);
 318             GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
 319             if (!predtoabstractmap.containsKey(tp))
 320                 predtoabstractmap.put(tp,new HashSet());
 321             ((Set)predtoabstractmap.get(tp)).add(gn);
 322             abstractrepair.add(gn);
 323             abstractrepairadd.add(gn);
 324             abstractadd.put(sd,gn);
 325
 326             DNFPredicate tp2=new DNFPredicate(true,ip);
 327             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
 328             TermNode tn2=new TermNode(ar2);
 329             GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
 330             if (!predtoabstractmap.containsKey(tp2))
 331                 predtoabstractmap.put(tp2,new HashSet());
 332             ((Set)predtoabstractmap.get(tp2)).add(gn2);
 333             abstractrepair.add(gn2);
 334             abstractrepairadd.add(gn2);
 335             abstractremove.put(sd,gn2);
 336         }
 337
 338         Vector relationdescriptors=state.stRelations.getAllDescriptors();
 339         for(int i=0;i<relationdescriptors.size();i++) {
 340             RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
 341
 342             /* XXXXXXX: Not sure what to do here */
 343             VarDescriptor vd1=new VarDescriptor("DUMMY1");
 344             VarExpr ve2=new VarExpr("DUMMY2");
 345
 346             InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
 347
 348             DNFPredicate tp=new DNFPredicate(false,ip);
 349             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
 350             TermNode tn=new TermNode(ar);
 351             GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
 352             if (!predtoabstractmap.containsKey(tp))
 353                 predtoabstractmap.put(tp,new HashSet());
 354             ((Set)predtoabstractmap.get(tp)).add(gn);
 355             abstractrepair.add(gn);
 356             abstractrepairadd.add(gn);
 357             abstractadd.put(rd,gn);
 358
 359             DNFPredicate tp2=new DNFPredicate(true,ip);
 360             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
 361             TermNode tn2=new TermNode(ar2);
 362             GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
 363             if (!predtoabstractmap.containsKey(tp2))
 364                 predtoabstractmap.put(tp2,new HashSet());
 365             ((Set)predtoabstractmap.get(tp2)).add(gn2);
 366             abstractrepair.add(gn2);
 367             abstractrepairadd.add(gn2);
 368             abstractremove.put(rd,gn2);
 369         }
 370
 371     }
 372
 373     int compensationcount=0;
 374     void generatecompensationnodes() {
 375         for(int i=0;i<state.vRules.size();i++) {
 376             Rule r=(Rule) state.vRules.get(i);
 377             Vector possiblerules=new Vector();
 378             /* Construct bindings */
 379             /* No need to construct bindings on remove
 380                Vector bindings=new Vector();
 381                constructbindings(bindings, r,true);
 382             */
 383             for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
 384                 GraphNode gn=(GraphNode)scopesatisfy.get(r);
 385                 TermNode tn=(TermNode) gn.getOwner();
 386                 ScopeNode sn=tn.getScope();
 387                 MultUpdateNode mun=new MultUpdateNode(sn);
 388                 TermNode tn2=new TermNode(mun);
 389                 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
 390                 UpdateNode un=new UpdateNode(r);
 391                 //              un.addBindings(bindings);
 392                 // Not necessary
 393                 if (j<r.numQuantifiers()) {
 394                     /* Remove quantifier */
 395                     Quantifier q=r.getQuantifier(j);
 396                     if (q instanceof RelationQuantifier) {
 397                         RelationQuantifier rq=(RelationQuantifier)q;
 398                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 399                         toe.td=ReservedTypeDescriptor.INT;
 400                         Updates u=new Updates(toe,true);
 401                         un.addUpdate(u);
 402                         if (abstractremove.containsKey(rq.relation)) {
 403                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 404                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 405                             gn2.addEdge(e);
 406                         } else {
 407                             continue; /* Abstract repair doesn't exist */
 408                         }
 409                     } else if (q instanceof SetQuantifier) {
 410                         SetQuantifier sq=(SetQuantifier)q;
 411                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 412                         eoe.td=ReservedTypeDescriptor.INT;
 413                         Updates u=new Updates(eoe,true);
 414                         un.addUpdate(u);
 415                         if (abstractremove.containsKey(sq.set)) {
 416                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 417                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 418                             gn2.addEdge(e);
 419                         } else {
 420                             continue; /* Abstract repair doesn't exist */
 421                         }
 422                     } else {
 423                         continue;
 424                     }
 425                 } else {
 426                     int c=j-r.numQuantifiers();
 427                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 428                         continue;
 429                     }
 430                 }
 431                 if (!un.checkupdates()) /* Make sure we have a good update */
 432                     continue;
 433
 434                 mun.addUpdate(un);
 435
 436                 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
 437                 compensationcount++;
 438                 gn.addEdge(e);
 439                 updatenodes.add(gn2);
 440             }
 441         }
 442     }
 443
 444     void generatedatastructureupdatenodes() {
 445         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 446             GraphNode gn=(GraphNode)absiterator.next();
 447             TermNode tn=(TermNode) gn.getOwner();
 448             AbstractRepair ar=tn.getAbstract();
 449             if (ar.getType()==AbstractRepair.ADDTOSET) {
 450                 generateaddtosetrelation(gn,ar);
 451             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 452                 generateremovefromsetrelation(gn,ar);
 453             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 454                 generateaddtosetrelation(gn,ar);
 455             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 456                 generateremovefromsetrelation(gn,ar);
 457             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 458                 /* Generate remove/add pairs */
 459                 generateremovefromsetrelation(gn,ar);
 460                 generateaddtosetrelation(gn,ar);
 461                 /* Generate atomic modify */
 462                 generatemodifyrelation(gn,ar);
 463             }
 464         }
 465     }
 466
 467     int removefromcount=0;
 468     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
 469         Vector possiblerules=new Vector();
 470         for(int i=0;i<state.vRules.size();i++) {
 471             Rule r=(Rule) state.vRules.get(i);
 472             if ((r.getInclusion() instanceof SetInclusion)&&
 473                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 474                 possiblerules.add(r);
 475             if ((r.getInclusion() instanceof RelationInclusion)&&
 476                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
 477                 possiblerules.add(r);
 478         }
 479         if (possiblerules.size()==0)
 480             return;
 481         int[] count=new int[possiblerules.size()];
 482         while(remains(count,possiblerules,true)) {
 483             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
 484             TermNode tn=new TermNode(mun);
 485             GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 486
 487             boolean goodflag=true;
 488             for(int i=0;i<possiblerules.size();i++) {
 489                 Rule r=(Rule)possiblerules.get(i);
 490                 UpdateNode un=new UpdateNode(r);
 491                 /* Construct bindings */
 492                 /* No Need to construct bindings on remove
 493                    Vector bindings=new Vector();
 494                    constructbindings(bindings, r,true);
 495                   un.addBindings(bindings);*/
 496                 if (count[i]<r.numQuantifiers()) {
 497                     /* Remove quantifier */
 498                     Quantifier q=r.getQuantifier(count[i]);
 499                     if (q instanceof RelationQuantifier) {
 500                         RelationQuantifier rq=(RelationQuantifier)q;
 501                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 502                         toe.td=ReservedTypeDescriptor.INT;
 503                         Updates u=new Updates(toe,true);
 504                         un.addUpdate(u);
 505                         if (abstractremove.containsKey(rq.relation)) {
 506                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 507                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 508                             gn2.addEdge(e);
 509                         } else {
 510                             goodflag=false;break; /* Abstract repair doesn't exist */
 511                         }
 512                     } else if (q instanceof SetQuantifier) {
 513                         SetQuantifier sq=(SetQuantifier)q;
 514                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 515                         eoe.td=ReservedTypeDescriptor.INT;
 516                         Updates u=new Updates(eoe,true);
 517                         un.addUpdate(u);
 518                         if (abstractremove.containsKey(sq.set)) {
 519                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 520                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 521                             gn2.addEdge(e);
 522                         } else {
 523                             goodflag=false;break; /* Abstract repair doesn't exist */
 524                         }
 525                     } else {goodflag=false;break;}
 526                 } else {
 527                     int c=count[i]-r.numQuantifiers();
 528                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 529                         goodflag=false;break;
 530                     }
 531                 }
 532                 if (!un.checkupdates()) {
 533                     goodflag=false;
 534                     break;
 535                 }
 536                 mun.addUpdate(un);
 537             }
 538             if (goodflag) {
 539                 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
 540                 removefromcount++;
 541                 gn.addEdge(e);
 542                 updatenodes.add(gn2);
 543             }
 544             increment(count,possiblerules,true);
 545         }
 546     }
 547
 548     static private void increment(int count[], Vector rules,boolean isremove) {
 549         count[0]++;
 550         for(int i=0;i<(rules.size()-1);i++) {
 551             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
 552             if (count[i]>=num) {
 553                 count[i+1]++;
 554                 count[i]=0;
 555             } else break;
 556         }
 557     }
 558
 559     static private boolean remains(int count[], Vector rules, boolean isremove) {
 560         for(int i=0;i<rules.size();i++) {
 561             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
 562             if (count[i]>=num) {
 563                 return false;
 564             }
 565         }
 566         return true;
 567     }
 568
 569     /** This method generates data structure updates to implement the
 570      *  abstract atomic modification specified by ar. */
 571     int modifycount=0;
 572     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
 573         RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
 574         ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
 575         boolean inverted=exprPredicate.inverted();
 576         int leftindex=0;
 577         int rightindex=1;
 578         if (inverted)
 579             leftindex=2;
 580         else
 581             rightindex=2;
 582
 583
 584         Vector possiblerules=new Vector();
 585         for(int i=0;i<state.vRules.size();i++) {
 586             Rule r=(Rule) state.vRules.get(i);
 587             if ((r.getInclusion() instanceof RelationInclusion)&&
 588                 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
 589                 possiblerules.add(r);
 590         }
 591         if (possiblerules.size()==0)
 592             return;
 593         int[] count=new int[possiblerules.size()];
 594         while(remains(count,possiblerules,false)) {
 595             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
 596             TermNode tn=new TermNode(mun);
 597             GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
 598
 599             boolean goodflag=true;
 600             for(int i=0;i<possiblerules.size();i++) {
 601                 Rule r=(Rule)possiblerules.get(i);
 602                 UpdateNode un=new UpdateNode(r);
 603                 /* No Need to construct bindings on modify */
 604
 605                 int c=count[i];
 606                 if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
 607                     goodflag=false;break;
 608                 }
 609                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
 610                 if (!(ri.getLeftExpr() instanceof VarExpr)) {
 611                     if (ri.getLeftExpr().isValue()) {
 612                         Updates up=new Updates(ri.getLeftExpr(),leftindex);
 613                         un.addUpdate(up);
 614                     } else
 615                         goodflag=false;
 616                 } else {
 617                     VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 618                     if (vd.isGlobal()) {
 619                         Updates up=new Updates(ri.getLeftExpr(),leftindex);
 620                         un.addUpdate(up);
 621                     } else if (inverted)
 622                         goodflag=false;
 623                 }
 624                 if (!(ri.getRightExpr() instanceof VarExpr)) {
 625                     if (ri.getRightExpr().isValue()) {
 626                         Updates up=new Updates(ri.getRightExpr(),rightindex);
 627                         un.addUpdate(up);
 628                     } else
 629                         goodflag=false;
 630                 } else {
 631                     VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 632                     if (vd.isGlobal()) {
 633                         Updates up=new Updates(ri.getRightExpr(),rightindex);
 634                         un.addUpdate(up);
 635                     } else if (!inverted)
 636                         goodflag=false;
 637                 }
 638
 639                 if (!un.checkupdates()) {
 640                     goodflag=false;
 641                     break;
 642                 }
 643                 mun.addUpdate(un);
 644             }
 645             if (goodflag) {
 646                 GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
 647                 modifycount++;
 648                 gn.addEdge(e);
 649                 updatenodes.add(gn2);
 650             }
 651             increment(count,possiblerules,false);
 652         }
 653     }
 654     /** This method constructs bindings for an update using rule
 655      * r. The boolean flag isremoval indicates that the update
 656      * performs a removal.  The function returns true if it is able to
 657      * generate a valid set of bindings and false otherwise. */
 658
 659     boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
 660         boolean goodupdate=true;
 661         Inclusion inc=r.getInclusion();
 662         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 663             Quantifier q=(Quantifier)iterator.next();
 664             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 665                 VarDescriptor vd=null;
 666                 SetDescriptor set=null;
 667                 if (q instanceof SetQuantifier) {
 668                     vd=((SetQuantifier)q).getVar();
 669                     set=((SetQuantifier)q).getSet();
 670                 } else {
 671                     vd=((ForQuantifier)q).getVar();
 672                 }
 673                 if(inc instanceof SetInclusion) {
 674                     SetInclusion si=(SetInclusion)inc;
 675                     if ((si.elementexpr instanceof VarExpr)&&
 676                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 677                         /* Can solve for v */
 678                         Binding binding=new Binding(vd,0);
 679                         bindings.add(binding);
 680                     } else {
 681                         goodupdate=false;
 682                     }
 683                 } else if (inc instanceof RelationInclusion) {
 684                     RelationInclusion ri=(RelationInclusion)inc;
 685                     boolean f1=true;
 686                     boolean f2=true;
 687                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 688                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 689                                 /* Can solve for v */
 690                         Binding binding=new Binding(vd,0);
 691                         bindings.add(binding);
 692                     } else f1=false;
 693                     if ((ri.getRightExpr() instanceof VarExpr)&&
 694                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 695                                 /* Can solve for v */
 696                         Binding binding=new Binding(vd,0);
 697                         bindings.add(binding);
 698                     } else f2=false;
 699                     if (!(f1||f2))
 700                         goodupdate=false;
 701                 } else throw new Error("Inclusion not recognized");
 702                 if (!goodupdate)
 703                     if (isremoval) {
 704                         /* Removals don't need bindings anymore
 705                            Binding binding=new Binding(vd);
 706                            bindings.add(binding);*/
 707                         goodupdate=true;
 708                     } else if (q instanceof SetQuantifier) {
 709                         /* Create new element to bind to */
 710                         // search if the set 'set' has a size
 711                         Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
 712                         bindings.add(binding);
 713                         goodupdate=true;
 714
 715                     } else
 716                         goodupdate=false;
 717             } else if (q instanceof RelationQuantifier) {
 718                 RelationQuantifier rq=(RelationQuantifier)q;
 719                 for(int k=0;k<2;k++) {
 720                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 721                     if(inc instanceof SetInclusion) {
 722                         SetInclusion si=(SetInclusion)inc;
 723                         if ((si.elementexpr instanceof VarExpr)&&
 724                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 725                             /* Can solve for v */
 726                             Binding binding=new Binding(vd,0);
 727                             bindings.add(binding);
 728                         } else
 729                             goodupdate=false;
 730                     } else if (inc instanceof RelationInclusion) {
 731                         RelationInclusion ri=(RelationInclusion)inc;
 732                         boolean f1=true;
 733                         boolean f2=true;
 734                         if ((ri.getLeftExpr() instanceof VarExpr)&&
 735                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 736                             /* Can solve for v */
 737                             Binding binding=new Binding(vd,0);
 738                             bindings.add(binding);
 739                         } else f1=false;
 740                         if ((ri.getRightExpr() instanceof VarExpr)&&
 741                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 742                             /* Can solve for v */
 743                             Binding binding=new Binding(vd,0);
 744                             bindings.add(binding);
 745                         } else f2=false;
 746                         if (!(f1||f2))
 747                             goodupdate=false;
 748                     } else throw new Error("Inclusion not recognized");
 749                     if (!goodupdate)
 750                         if (isremoval) {
 751                             /* Removals don't need bindings anymore
 752                                Binding binding=new Binding(vd);
 753                                bindings.add(binding);*/
 754                             goodupdate=true;
 755                         } else
 756                             break;
 757                 }
 758                 if (!goodupdate)
 759                     break;
 760             } else throw new Error("Quantifier not recognized");
 761         }
 762         return goodupdate;
 763     }
 764
 765     static int addtocount=0;
 766     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
 767         for(int i=0;i<state.vRules.size();i++) {
 768             Rule r=(Rule) state.vRules.get(i);
 769             /* See if this is a good rule*/
 770             if ((r.getInclusion() instanceof SetInclusion&&
 771                  ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 772                 (r.getInclusion() instanceof RelationInclusion&&
 773                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 774
 775                 /* First solve for quantifiers */
 776                 Vector bindings=new Vector();
 777                 /* Construct bindings */
 778                 if (!constructbindings(bindings,r,false))
 779                     continue;
 780                 //Generate add instruction
 781                 DNFRule dnfrule=r.getDNFGuardExpr();
 782                 for(int j=0;j<dnfrule.size();j++) {
 783                     Inclusion inc=r.getInclusion();
 784                     UpdateNode un=new UpdateNode(r);
 785                     un.addBindings(bindings);
 786                     /* Now build update for tuple/set inclusion condition */
 787                     if(inc instanceof SetInclusion) {
 788                         SetInclusion si=(SetInclusion)inc;
 789                         if (!(si.elementexpr instanceof VarExpr)) {
 790                             if (si.elementexpr.isValue()) {
 791                                 Updates up=new Updates(si.elementexpr,0);
 792                                 un.addUpdate(up);
 793                             } else
 794                                 continue;
 795                         } else {
 796                             VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 797                             if (vd.isGlobal()) {
 798                                 Updates up=new Updates(si.elementexpr,0);
 799                                 un.addUpdate(up);
 800                             }
 801                         }
 802                     } else if (inc instanceof RelationInclusion) {
 803                         RelationInclusion ri=(RelationInclusion)inc;
 804                         if (!(ri.getLeftExpr() instanceof VarExpr)) {
 805                             if (ri.getLeftExpr().isValue()) {
 806                                 Updates up=new Updates(ri.getLeftExpr(),0);
 807                                 un.addUpdate(up);
 808                             } else
 809                                 continue;
 810                         } else {
 811                             VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 812                             if (vd.isGlobal()) {
 813                                 Updates up=new Updates(ri.getLeftExpr(),0);
 814                                 un.addUpdate(up);
 815                             }
 816                         }
 817                         if (!(ri.getRightExpr() instanceof VarExpr)) {
 818                             if (ri.getRightExpr().isValue()) {
 819                                 Updates up=new Updates(ri.getRightExpr(),1);
 820                                 un.addUpdate(up);
 821                             } else
 822                                 continue;
 823                         } else {
 824                             VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 825                             if (vd.isGlobal()) {
 826                                 Updates up=new Updates(ri.getRightExpr(),1);
 827                                 un.addUpdate(up);
 828                             }
 829                         }
 830                     }
 831                     //Finally build necessary updates to satisfy conjunction
 832                     RuleConjunction ruleconj=dnfrule.get(j);
 833
 834                     /* Add in updates for quantifiers */
 835                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
 836                     TermNode tn=new TermNode(mun);
 837                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 838
 839                     if (processquantifiers(gn2,un, r)&&
 840                         processconjunction(un,ruleconj)&&
 841                         un.checkupdates()) {
 842                         mun.addUpdate(un);
 843                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 844                         addtocount++;
 845                         gn.addEdge(e);
 846                         updatenodes.add(gn2);
 847                     }
 848                 }
 849             }
 850         }
 851     }
 852
 853     /** Adds updates that add an item to the appropriate set or
 854      * relation quantified over by the model definition rule.. */
 855
 856     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) {
 857         Inclusion inc=r.getInclusion();
 858         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 859             Quantifier q=(Quantifier)iterator.next();
 860             /* Add quantifier */
 861             /* FIXME: Analysis to determine when this update is necessary */
 862             if (q instanceof RelationQuantifier) {
 863                 RelationQuantifier rq=(RelationQuantifier)q;
 864                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 865                 toe.td=ReservedTypeDescriptor.INT;
 866                 Updates u=new Updates(toe,false);
 867                 un.addUpdate(u);
 868                 if (abstractadd.containsKey(rq.relation)) {
 869                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
 870                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 871                     gn.addEdge(e);
 872                 } else {
 873                     return false;
 874                 }
 875
 876             } else if (q instanceof SetQuantifier) {
 877                 SetQuantifier sq=(SetQuantifier)q;
 878                 if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
 879                     Binding b=un.getBinding(sq.var);
 880                     Constraint reqc=exactsize.getConstraint(b.getSet());
 881                     constraintdependence.requiresConstraint(gn,reqc);
 882                     continue; /* Don't need to ensure addition for search */
 883                 }
 884
 885                 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 886                 eoe.td=ReservedTypeDescriptor.INT;
 887                 Updates u=new Updates(eoe,false);
 888                 un.addUpdate(u);
 889                 if (abstractadd.containsKey(sq.set)) {
 890                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
 891                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 892                     gn.addEdge(e);
 893                 } else {
 894                     return false;
 895                 }
 896             } else return false;
 897         }
 898         return true;
 899     }
 900
 901     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
 902         boolean okay=true;
 903         for(int k=0;k<ruleconj.size();k++) {
 904             DNFExpr de=ruleconj.get(k);
 905             Expr e=de.getExpr();
 906             if (e instanceof OpExpr) {
 907                 OpExpr ex=(OpExpr)de.getExpr();
 908                 Opcode op=ex.getOpcode();
 909                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
 910                 un.addUpdate(up);
 911             } else if (e instanceof ElementOfExpr) {
 912                 Updates up=new Updates(e,de.getNegation());
 913                 un.addUpdate(up);
 914             } else if (e instanceof TupleOfExpr) {
 915                 Updates up=new Updates(e,de.getNegation());
 916                 un.addUpdate(up);
 917             } else if (e instanceof BooleanLiteralExpr) {
 918                 boolean truth=((BooleanLiteralExpr)e).getValue();
 919                 if (de.getNegation())
 920                     truth=!truth;
 921                 if (!truth) {
 922                     okay=false;
 923                     break;
 924                 }
 925             } else {
 926                 System.out.println(e.getClass().getName());
 927                 throw new Error("Unrecognized Expr");
 928             }
 929         }
 930         return okay;
 931     }
 932
 933     void generatescopenodes() {
 934         for(int i=0;i<state.vRules.size();i++) {
 935             Rule r=(Rule) state.vRules.get(i);
 936             ScopeNode satisfy=new ScopeNode(r,true);
 937             TermNode tnsatisfy=new TermNode(satisfy);
 938             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 939             ConsequenceNode cnsatisfy=new ConsequenceNode();
 940             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 941             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 942             consequence.put(satisfy,cgnsatisfy);
 943             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 944             gnsatisfy.addEdge(esat);
 945             consequencenodes.add(cgnsatisfy);
 946             scopesatisfy.put(r,gnsatisfy);
 947             scopenodes.add(gnsatisfy);
 948
 949             ScopeNode falsify=new ScopeNode(r,false);
 950             TermNode tnfalsify=new TermNode(falsify);
 951             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 952             ConsequenceNode cnfalsify=new ConsequenceNode();
 953             TermNode ctnfalsify=new TermNode(cnfalsify);
 954             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 955             consequence.put(falsify,cgnfalsify);
 956             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 957             gnfalsify.addEdge(efals);
 958             consequencenodes.add(cgnfalsify);
 959             scopefalsify.put(r,gnfalsify);
 960             scopenodes.add(gnfalsify);
 961         }
 962     }
 963 }