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