Repair/RepairCompiler/MCC/IR/RepairGenerator.java

   1 package MCC.IR;
   2
   3 import java.io.*;
   4 import java.util.*;
   5 import MCC.State;
   6
   7 public class RepairGenerator {
   8     State state;
   9     java.io.PrintWriter outputrepair = null;
  10     java.io.PrintWriter outputaux = null;
  11     java.io.PrintWriter outputhead = null;
  12     String name="foo";
  13     String headername;
  14     static VarDescriptor oldmodel=null;
  15     static VarDescriptor newmodel=null;
  16     static VarDescriptor worklist=null;
  17     static VarDescriptor repairtable=null;
  18     static VarDescriptor goodflag=null;
  19     Rule currentrule=null;
  20     Hashtable updatenames;
  21     HashSet usedupdates;
  22     Termination termination;
  23     Set removed;
  24     HashSet togenerate;
  25     static boolean DEBUG=false;
  26     Cost cost;
  27     Sources sources;
  28
  29     public RepairGenerator(State state, Termination t) {
  30         this.state = state;
  31         updatenames=new Hashtable();
  32         usedupdates=new HashSet();
  33         termination=t;
  34         removed=t.removedset;
  35         togenerate=new HashSet();
  36         togenerate.addAll(termination.conjunctions);
  37         togenerate.removeAll(removed);
  38         GraphNode.computeclosure(togenerate,removed);
  39
  40         cost=new Cost();
  41         sources=new Sources(state);
  42         Repair.repairgenerator=this;
  43     }
  44
  45     private void name_updates() {
  46         int count=0;
  47         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  48             GraphNode gn=(GraphNode) it.next();
  49             TermNode tn=(TermNode) gn.getOwner();
  50             MultUpdateNode mun=tn.getUpdate();
  51             if (togenerate.contains(gn))
  52             for (int i=0;i<mun.numUpdates();i++) {
  53                 UpdateNode un=mun.getUpdate(i);
  54                 String name="update"+String.valueOf(count++);
  55                 updatenames.put(un,name);
  56             }
  57         }
  58     }
  59
  60     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
  61         this.outputrepair = new java.io.PrintWriter(outputrepair, true);
  62         this.outputaux = new java.io.PrintWriter(outputaux, true);
  63         this.outputhead = new java.io.PrintWriter(outputhead, true);
  64         headername=st;
  65         name_updates();
  66
  67         generate_tokentable();
  68         generate_hashtables();
  69         generate_stateobject();
  70         generate_call();
  71         generate_worklist();
  72         generate_rules();
  73         generate_checks();
  74         generate_teardown();
  75         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
  76         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  77         crhead.outputline("};");
  78         craux.outputline("};");
  79         generate_updates();
  80     }
  81
  82     private void generate_updates() {
  83         int count=0;
  84         CodeWriter crhead = new StandardCodeWriter(outputhead);
  85         CodeWriter craux = new StandardCodeWriter(outputaux);
  86         String state="state";
  87         String model="model";
  88         String repairtable="repairtable";
  89         String left="left";
  90         String right="right";
  91         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  92             GraphNode gn=(GraphNode) it.next();
  93             TermNode tn=(TermNode) gn.getOwner();
  94             MultUpdateNode mun=tn.getUpdate();
  95             boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
  96             if (togenerate.contains(gn))
  97             for (int i=0;i<mun.numUpdates();i++) {
  98                 UpdateNode un=mun.getUpdate(i);
  99                 String methodname=(String)updatenames.get(un);
 100
 101                 switch(mun.op) {
 102                 case MultUpdateNode.ADD:
 103                     if (isrelation) {
 104                         crhead.outputline("void "+methodname+"("+name+"_state * " +state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+");");
 105                         craux.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+")");
 106                     } else {
 107                         crhead.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+");");
 108                         craux.outputline("void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+")");
 109                     }
 110                     craux.startblock();
 111                     un.generate(craux, false, left,right);
 112                     craux.endblock();
 113                     break;
 114                 case MultUpdateNode.REMOVE:
 115                     Rule r=un.getRule();
 116                     String methodcall="void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable;
 117                     for(int j=0;j<r.numQuantifiers();j++) {
 118                         Quantifier q=r.getQuantifier(j);
 119                         if (q instanceof SetQuantifier) {
 120                             SetQuantifier sq=(SetQuantifier) q;
 121                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 122                         } else if (q instanceof RelationQuantifier) {
 123                             RelationQuantifier rq=(RelationQuantifier) q;
 124
 125                             methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 126                             methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 127                         } else if (q instanceof ForQuantifier) {
 128                             ForQuantifier fq=(ForQuantifier) q;
 129                             methodcall+=",int "+fq.getVar().getSafeSymbol();
 130                         }
 131                     }
 132                     methodcall+=")";
 133                     crhead.outputline(methodcall+";");
 134                     craux.outputline(methodcall);
 135                     craux.startblock();
 136                     un.generate(craux, true, null,null);
 137                     craux.endblock();
 138                     break;
 139                 case MultUpdateNode.MODIFY:
 140                 default:
 141                     throw new Error("Nonimplement Update");
 142                 }
 143             }
 144         }
 145     }
 146
 147     private void generate_call() {
 148         CodeWriter cr = new StandardCodeWriter(outputrepair);
 149         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
 150         cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
 151         Iterator globals=state.stGlobals.descriptors();
 152         while (globals.hasNext()) {
 153             VarDescriptor vd=(VarDescriptor) globals.next();
 154             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
 155         }
 156         /* Insert repair here */
 157         cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
 158         globals=state.stGlobals.descriptors();
 159         while (globals.hasNext()) {
 160             VarDescriptor vd=(VarDescriptor) globals.next();
 161             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
 162         }
 163         cr.outputline("delete "+vdstate.getSafeSymbol()+";");
 164     }
 165
 166     private void generate_tokentable() {
 167         CodeWriter cr = new StandardCodeWriter(outputrepair);
 168         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
 169
 170         cr.outputline("");
 171         cr.outputline("// Token values");
 172         cr.outputline("");
 173
 174         while (tokens.hasNext()) {
 175             Object token = tokens.next();
 176             cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
 177         }
 178
 179         cr.outputline("");
 180         cr.outputline("");
 181     }
 182
 183     private void generate_stateobject() {
 184         CodeWriter crhead = new StandardCodeWriter(outputhead);
 185         crhead.outputline("class "+name+"_state {");
 186         crhead.outputline("public:");
 187         Iterator globals=state.stGlobals.descriptors();
 188         while (globals.hasNext()) {
 189             VarDescriptor vd=(VarDescriptor) globals.next();
 190             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 191         }
 192     }
 193
 194     private void generate_hashtables() {
 195         CodeWriter craux = new StandardCodeWriter(outputaux);
 196         CodeWriter crhead = new StandardCodeWriter(outputhead);
 197         crhead.outputline("#include \"SimpleHash.h\"");
 198         crhead.outputline("#include <stdio.h>");
 199         crhead.outputline("#include <stdlib.h>");
 200         crhead.outputline("class "+name+" {");
 201         crhead.outputline("public:");
 202         crhead.outputline(name+"();");
 203         crhead.outputline("~"+name+"();");
 204         craux.outputline("#include \""+headername+"\"");
 205
 206         craux.outputline(name+"::"+name+"() {");
 207         craux.outputline("// creating hashtables ");
 208
 209         /* build sets */
 210         Iterator sets = state.stSets.descriptors();
 211
 212         /* first pass create all the hash tables */
 213         while (sets.hasNext()) {
 214             SetDescriptor set = (SetDescriptor) sets.next();
 215             crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
 216             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
 217         }
 218
 219         /* second pass build relationships between hashtables */
 220         sets = state.stSets.descriptors();
 221
 222         while (sets.hasNext()) {
 223             SetDescriptor set = (SetDescriptor) sets.next();
 224             Iterator subsets = set.subsets();
 225
 226             while (subsets.hasNext()) {
 227                 SetDescriptor subset = (SetDescriptor) subsets.next();
 228                 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
 229             }
 230         }
 231
 232         /* build relations */
 233         Iterator relations = state.stRelations.descriptors();
 234
 235         /* first pass create all the hash tables */
 236         while (relations.hasNext()) {
 237             RelationDescriptor relation = (RelationDescriptor) relations.next();
 238
 239             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 240                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
 241                 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
 242             }
 243
 244             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 245                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
 246                 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
 247             }
 248         }
 249
 250         craux.outputline("}");
 251         crhead.outputline("};");
 252         craux.outputline(name+"::~"+name+"() {");
 253         craux.outputline("// deleting hashtables");
 254
 255         /* build destructor */
 256         sets = state.stSets.descriptors();
 257
 258         /* first pass create all the hash tables */
 259         while (sets.hasNext()) {
 260             SetDescriptor set = (SetDescriptor) sets.next();
 261             craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
 262         }
 263
 264         /* destroy relations */
 265         relations = state.stRelations.descriptors();
 266
 267         /* first pass create all the hash tables */
 268         while (relations.hasNext()) {
 269             RelationDescriptor relation = (RelationDescriptor) relations.next();
 270
 271             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 272                 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
 273             }
 274
 275             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 276                 craux.outputline("delete " + relation.getSafeSymbol() + ";");
 277             }
 278         }
 279         craux.outputline("}");
 280     }
 281
 282     private void generate_worklist() {
 283         CodeWriter crhead = new StandardCodeWriter(outputhead);
 284         CodeWriter craux = new StandardCodeWriter(outputaux);
 285         oldmodel=VarDescriptor.makeNew("oldmodel");
 286         newmodel=VarDescriptor.makeNew("newmodel");
 287         worklist=VarDescriptor.makeNew("worklist");
 288         goodflag=VarDescriptor.makeNew("goodflag");
 289         repairtable=VarDescriptor.makeNew("repairtable");
 290         crhead.outputline("void doanalysis();");
 291         craux.outputline("void "+name +"_state::doanalysis()");
 292         craux.startblock();
 293         craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
 294         craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
 295         craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 296         craux.outputline("while (1)");
 297         craux.startblock();
 298         craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
 299         craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
 300     }
 301
 302     private void generate_teardown() {
 303         CodeWriter cr = new StandardCodeWriter(outputaux);
 304         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 305         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 306         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 307         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 308         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
 309         cr.outputline("delete "+worklist.getSafeSymbol()+";");
 310         cr.endblock();
 311     }
 312
 313     private void generate_rules() {
 314         /* first we must sort the rules */
 315         Iterator allrules = state.vRules.iterator();
 316         Vector emptyrules = new Vector(); // rules with no quantifiers
 317         Vector worklistrules = new Vector(); // the rest of the rules
 318         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 319         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 320
 321         while (allrules.hasNext()) {
 322             Rule rule = (Rule) allrules.next();
 323             ListIterator quantifiers = rule.quantifiers();
 324             boolean noquantifiers = true;
 325             while (quantifiers.hasNext()) {
 326                 Quantifier quantifier = (Quantifier) quantifiers.next();
 327                 if (quantifier instanceof ForQuantifier) {
 328                     // ok, because integers exist already!
 329                 } else {
 330                     // real quantifier
 331                     noquantifiers = false;
 332                     break;
 333                 }
 334             }
 335             if (noquantifiers) {
 336                 emptyrules.add(rule);
 337             } else {
 338                 worklistrules.add(rule);
 339             }
 340         }
 341
 342         Iterator iterator_er = emptyrules.iterator();
 343         while (iterator_er.hasNext()) {
 344             Rule rule = (Rule) iterator_er.next();
 345             {
 346                 final SymbolTable st = rule.getSymbolTable();
 347                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 348                         public SymbolTable getSymbolTable() { return st; }
 349                     };
 350                 cr.outputline("// build " +escape(rule.toString()));
 351                 cr.startblock();
 352                 ListIterator quantifiers = rule.quantifiers();
 353                 while (quantifiers.hasNext()) {
 354                     Quantifier quantifier = (Quantifier) quantifiers.next();
 355                     quantifier.generate_open(cr);
 356                 }
 357
 358                 /* pretty print! */
 359                 cr.output("//");
 360                 rule.getGuardExpr().prettyPrint(cr);
 361                 cr.outputline("");
 362
 363                 /* now we have to generate the guard test */
 364                 VarDescriptor guardval = VarDescriptor.makeNew();
 365                 rule.getGuardExpr().generate(cr, guardval);
 366                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 367                 cr.startblock();
 368
 369                 /* now we have to generate the inclusion code */
 370                 currentrule=rule;
 371                 rule.getInclusion().generate(cr);
 372                 cr.endblock();
 373                 while (quantifiers.hasPrevious()) {
 374                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 375                     cr.endblock();
 376                 }
 377                 cr.endblock();
 378                 cr.outputline("");
 379                 cr.outputline("");
 380             }
 381         }
 382
 383         CodeWriter cr2 = new StandardCodeWriter(outputaux);
 384
 385         cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
 386         cr2.startblock();
 387         VarDescriptor idvar=VarDescriptor.makeNew("id");
 388         cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
 389
 390         String elseladder = "if";
 391
 392         Iterator iterator_rules = worklistrules.iterator();
 393         while (iterator_rules.hasNext()) {
 394
 395             Rule rule = (Rule) iterator_rules.next();
 396             int dispatchid = rule.getNum();
 397
 398             {
 399                 final SymbolTable st = rule.getSymbolTable();
 400                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 401                         public SymbolTable getSymbolTable() { return st; }
 402                     };
 403
 404                 cr.indent();
 405                 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 406                 cr.startblock();
 407                 VarDescriptor typevar=VarDescriptor.makeNew("type");
 408                 VarDescriptor leftvar=VarDescriptor.makeNew("left");
 409                 VarDescriptor rightvar=VarDescriptor.makeNew("right");
 410                 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
 411                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
 412                 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
 413                 cr.outputline("// build " +escape(rule.toString()));
 414
 415
 416                 for (int j=0;j<rule.numQuantifiers();j++) {
 417                     Quantifier quantifier = rule.getQuantifier(j);
 418                     quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 419                 }
 420
 421                 /* pretty print! */
 422                 cr.output("//");
 423
 424                 rule.getGuardExpr().prettyPrint(cr);
 425                 cr.outputline("");
 426
 427                 /* now we have to generate the guard test */
 428
 429                 VarDescriptor guardval = VarDescriptor.makeNew();
 430                 rule.getGuardExpr().generate(cr, guardval);
 431
 432                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 433                 cr.startblock();
 434
 435                 /* now we have to generate the inclusion code */
 436                 currentrule=rule;
 437                 rule.getInclusion().generate(cr);
 438                 cr.endblock();
 439
 440                 for (int j=0;j<rule.numQuantifiers();j++) {
 441                     cr.endblock();
 442                 }
 443
 444                 // close startblocks generated by DotExpr memory checks
 445                 //DotExpr.generate_memory_endblocks(cr);
 446
 447                 cr.endblock(); // end else-if WORKLIST ladder
 448
 449                 elseladder = "else if";
 450             }
 451         }
 452
 453         cr2.outputline("else");
 454         cr2.startblock();
 455         cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 456         cr2.outputline("exit(1);");
 457         cr2.endblock();
 458         // end block created for worklist
 459         cr2.endblock();
 460     }
 461
 462     public static String escape(String s) {
 463         String newstring="";
 464         for(int i=0;i<s.length();i++) {
 465             char c=s.charAt(i);
 466             if (c=='"')
 467                 newstring+="\"";
 468             else
 469                 newstring+=c;
 470         }
 471         return newstring;
 472     }
 473
 474     private void generate_checks() {
 475
 476         /* do constraint checks */
 477         Vector constraints = state.vConstraints;
 478
 479         for (int i = 0; i < constraints.size(); i++) {
 480
 481             Constraint constraint = (Constraint) constraints.elementAt(i);
 482
 483             {
 484
 485                 final SymbolTable st = constraint.getSymbolTable();
 486
 487                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 488                         public SymbolTable getSymbolTable() { return st; }
 489                     };
 490
 491                 cr.outputline("// checking " + escape(constraint.toString()));
 492                 cr.startblock();
 493
 494                 ListIterator quantifiers = constraint.quantifiers();
 495
 496                 while (quantifiers.hasNext()) {
 497                     Quantifier quantifier = (Quantifier) quantifiers.next();
 498                     quantifier.generate_open(cr);
 499                 }
 500
 501                 cr.outputline("int maybe = 0;");
 502
 503                 /* now we have to generate the guard test */
 504
 505                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 506                 constraint.getLogicStatement().generate(cr, constraintboolean);
 507
 508                 cr.outputline("if (maybe)");
 509                 cr.startblock();
 510                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \");");
 511                 cr.outputline("exit(1);");
 512                 cr.endblock();
 513
 514                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 515                 cr.startblock();
 516                 if (DEBUG)
 517                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
 518
 519                 /* Do repairs */
 520                 /* Build new repair table */
 521                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 522                 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 523                 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
 524
 525
 526                 /* Compute cost of each repair */
 527                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 528                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 529                 DNFConstraint dnfconst=constraint.dnfconstraint;
 530                 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
 531                 if (dnfconst.size()>1) {
 532                     boolean first=true;
 533                     for(int j=0;j<dnfconst.size();j++) {
 534                         Conjunction conj=dnfconst.get(j);
 535                         GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 536                         if (removed.contains(gn))
 537                             continue;
 538
 539                         VarDescriptor costvar;
 540                         if (first) {
 541                             costvar=mincost;
 542                         } else
 543                             costvar=VarDescriptor.makeNew("cost");
 544                         for(int k=0;k<conj.size();k++) {
 545                             DNFPredicate dpred=conj.get(k);
 546                             Predicate p=dpred.getPredicate();
 547                             boolean negate=dpred.isNegated();
 548                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 549                             p.generate(cr,predvalue);
 550                             if (negate)
 551                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 552                             else
 553                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 554                             if (k==0)
 555                                 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
 556                             else
 557                                 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 558                         }
 559
 560                         if(!first) {
 561                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
 562                             cr.startblock();
 563                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
 564                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 565                             cr.endblock();
 566                         } else
 567                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 568                         first=false;
 569                     }
 570                 }
 571                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
 572                 for(int j=0;j<dnfconst.size();j++) {
 573                     Conjunction conj=dnfconst.get(j);
 574                     GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);                    if (removed.contains(gn))
 575                         continue;
 576                     cr.outputline("case "+j+":");
 577                     for(int k=0;k<conj.size();k++) {
 578                         DNFPredicate dpred=conj.get(k);
 579                         Predicate p=dpred.getPredicate();
 580                         boolean negate=dpred.isNegated();
 581                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 582                         p.generate(cr,predvalue);
 583                         if (negate)
 584                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 585                         else
 586                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 587                         cr.startblock();
 588                         if (p instanceof InclusionPredicate)
 589                             generateinclusionrepair(conj,dpred, cr);
 590                         else if (p instanceof ExprPredicate) {
 591                             ExprPredicate ep=(ExprPredicate)p;
 592                             if (ep.getType()==ExprPredicate.SIZE)
 593                                 generatesizerepair(conj,dpred,cr);
 594                             else if (ep.getType()==ExprPredicate.COMPARISON)
 595                                 generatecomparisonrepair(conj,dpred,cr);
 596                         } else throw new Error("Unrecognized Predicate");
 597                         cr.endblock();
 598                     }
 599                     /* Update model */
 600
 601                     cr.outputline("break;");
 602                 }
 603                 cr.outputline("}");
 604
 605                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
 606                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 607                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 608                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
 609                 cr.outputline("break;");  /* Rebuild model and all */
 610
 611                 cr.endblock();
 612
 613                 while (quantifiers.hasPrevious()) {
 614                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 615                     cr.endblock();
 616                 }
 617                 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
 618                 cr.outputline("break;");
 619                 cr.endblock();
 620                 cr.outputline("");
 621                 cr.outputline("");
 622             }
 623         }
 624     }
 625
 626     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
 627         MultUpdateNode mun=null;
 628         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
 629         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
 630             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 631             TermNode tn2=(TermNode)gn2.getOwner();
 632             if (tn2.getType()==TermNode.ABSTRACT) {
 633                 AbstractRepair ar=tn2.getAbstract();
 634                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
 635                     ar.getPredicate()==dpred) {
 636                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 637                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
 638                         if (!removed.contains(gn3)) {
 639                             TermNode tn3=(TermNode)gn3.getOwner();
 640                             if (tn3.getType()==TermNode.UPDATE) {
 641                                 mun=tn3.getUpdate();
 642                                 break;
 643                             }
 644                         }
 645                     }
 646                 }
 647             }
 648         }
 649         return mun;
 650     }
 651
 652     public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 653         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 654         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 655         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 656         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
 657         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 658         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 659         boolean inverted=ep.inverted();
 660         boolean negated=dpred.isNegated();
 661         OpExpr expr=(OpExpr)ep.expr;
 662         Opcode opcode=expr.getOpcode();
 663         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 664         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 665         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
 666         if (!inverted) {
 667             expr.getLeftExpr().generate(cr,leftside);
 668             expr.getRightExpr().generate(cr,newvalue);
 669             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
 670             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 671         } else {
 672             expr.getLeftExpr().generate(cr,rightside);
 673             expr.getRightExpr().generate(cr,newvalue);
 674             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 675             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 676         }
 677         if (negated)
 678             if (opcode==Opcode.GT) {
 679                 opcode=Opcode.LE;
 680             } else if (opcode==Opcode.GE) {
 681                 opcode=Opcode.LT;
 682             } else if (opcode==Opcode.LT) {
 683                 opcode=Opcode.GE;
 684             } else if (opcode==Opcode.LE) {
 685                 opcode=Opcode.GT;
 686             } else if (opcode==Opcode.EQ) {
 687                 opcode=Opcode.NE;
 688             } else if (opcode==Opcode.NE) {
 689                 opcode=Opcode.EQ;
 690             } else {
 691                 throw new Error("Unrecognized Opcode");
 692             }
 693
 694         if (opcode==Opcode.GT) {
 695             cr.outputline(newvalue.getSafeSymbol()+"++;");
 696         } else if (opcode==Opcode.GE) {
 697             /* Equal */
 698         } else if (opcode==Opcode.LT) {
 699             cr.outputline(newvalue.getSafeSymbol()+"--;");
 700         } else if (opcode==Opcode.LE) {
 701             /* Equal */
 702         } else if (opcode==Opcode.EQ) {
 703             /* Equal */
 704         } else if (opcode==Opcode.NE) {
 705             cr.outputline(newvalue.getSafeSymbol()+"++;");
 706         } else {
 707             throw new Error("Unrecognized Opcode");
 708         }
 709         /* Do abstract repairs */
 710         if (usageimage) {
 711             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 712             if (!inverted) {
 713                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 714             } else {
 715                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 716             }
 717         }
 718         if (usageinvimage) {
 719             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 720             if (!inverted) {
 721                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 722             } else {
 723                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 724             }
 725         }
 726         /* Do concrete repairs */
 727         /* Start with scheduling removal */
 728         for(int i=0;i<state.vRules.size();i++) {
 729             Rule r=(Rule)state.vRules.get(i);
 730             if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 731                 for(int j=0;j<munremove.numUpdates();j++) {
 732                     UpdateNode un=munremove.getUpdate(i);
 733                     if (un.getRule()==r) {
 734                         /* Update for rule r */
 735                         String name=(String)updatenames.get(un);
 736                         cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
 737                     }
 738                 }
 739             }
 740         }
 741         /* Now do addition */
 742         UpdateNode un=munadd.getUpdate(0);
 743         String name=(String)updatenames.get(un);
 744         if (!inverted) {
 745             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 746         } else {
 747             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 748         }
 749     }
 750
 751     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
 752         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 753         OpExpr expr=(OpExpr)ep.expr;
 754         Opcode opcode=expr.getOpcode();
 755         {
 756             boolean negated=dpred.isNegated();
 757             if (negated)
 758                 if (opcode==Opcode.GT) {
 759                     opcode=Opcode.LE;
 760                 } else if (opcode==Opcode.GE) {
 761                     opcode=Opcode.LT;
 762                 } else if (opcode==Opcode.LT) {
 763                     opcode=Opcode.GE;
 764                 } else if (opcode==Opcode.LE) {
 765                     opcode=Opcode.GT;
 766                 } else if (opcode==Opcode.EQ) {
 767                     opcode=Opcode.NE;
 768                 } else if (opcode==Opcode.NE) {
 769                     opcode=Opcode.EQ;
 770                 } else {
 771                     throw new Error("Unrecognized Opcode");
 772                 }
 773         }
 774         MultUpdateNode munremove;
 775
 776         MultUpdateNode munadd;
 777         if (ep.getDescriptor() instanceof RelationDescriptor) {
 778             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 779             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 780         } else {
 781             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
 782             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
 783         }
 784         int size=ep.leftsize();
 785         VarDescriptor sizevar=VarDescriptor.makeNew("size");
 786         ((OpExpr)expr).left.generate(cr, sizevar);
 787         VarDescriptor change=VarDescriptor.makeNew("change");
 788         cr.outputline("int "+change.getSafeSymbol()+";");
 789         boolean generateadd=false;
 790         boolean generateremove=false;
 791         if (opcode==Opcode.GT) {
 792             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 793             generateadd=true;
 794             generateremove=false;
 795         } else if (opcode==Opcode.GE) {
 796             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 797             generateadd=true;
 798             generateremove=false;
 799         } else if (opcode==Opcode.LT) {
 800             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
 801             generateadd=false;
 802             generateremove=true;
 803         } else if (opcode==Opcode.LE) {
 804             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 805             generateadd=false;
 806             generateremove=true;
 807         } else if (opcode==Opcode.EQ) {
 808             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 809             generateadd=true;
 810             generateremove=true;
 811         } else if (opcode==Opcode.NE) {
 812             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 813             generateadd=true;
 814             generateremove=false;
 815         } else {
 816             throw new Error("Unrecognized Opcode");
 817         }
 818         Descriptor d=ep.getDescriptor();
 819         if (generateremove) {
 820             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
 821             cr.startblock();
 822             /* Find element to remove */
 823             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
 824             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
 825             if (d instanceof RelationDescriptor) {
 826                 if (ep.inverted()) {
 827                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 828                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
 829                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
 830                 } else {
 831                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 832                     cr.outputline("int "+rightvar.getSafeSymbol()+";");
 833                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
 834                 }
 835             } else {
 836                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
 837             }
 838             /* Generate abstract remove instruction */
 839             if (d instanceof RelationDescriptor) {
 840                 RelationDescriptor rd=(RelationDescriptor) d;
 841                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 842                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 843                 if (usageimage)
 844                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 845                 if (usageinvimage)
 846                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 847             } else {
 848                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
 849             }
 850             /* Generate concrete remove instruction */
 851             for(int i=0;i<state.vRules.size();i++) {
 852                 Rule r=(Rule)state.vRules.get(i);
 853                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
 854                     for(int j=0;j<munremove.numUpdates();j++) {
 855                         UpdateNode un=munremove.getUpdate(i);
 856                         if (un.getRule()==r) {
 857                                 /* Update for rule rule r */
 858                             String name=(String)updatenames.get(un);
 859                             if (d instanceof RelationDescriptor) {
 860                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
 861                             } else {
 862                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
 863                             }
 864                         }
 865                     }
 866                 }
 867             }
 868             cr.endblock();
 869         }
 870         if (generateadd) {
 871
 872             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
 873             cr.startblock();
 874             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
 875             if (d instanceof RelationDescriptor) {
 876                 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
 877                 RelationDescriptor rd=(RelationDescriptor)d;
 878                 if (sources.relsetSource(rd,!ep.inverted())) {
 879                     /* Set Source */
 880                     SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
 881                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
 882                     cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
 883                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
 884                     cr.startblock();
 885                     if (ep.inverted()) {
 886                         cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
 887                     } else {
 888                         cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
 889                     }
 890                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
 891                     cr.outputline(iterator.getSafeSymbol()+"->next();");
 892                     cr.endblock();
 893                 } else if (sources.relallocSource(rd,!ep.inverted())) {
 894                     /* Allocation Source*/
 895                     sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
 896                 } else throw new Error("No source for adding to Relation");
 897                 if (ep.inverted()) {
 898                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 899                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 900                     if (usageimage)
 901                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
 902                     if (usageinvimage)
 903                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
 904
 905                     UpdateNode un=munadd.getUpdate(0);
 906                     String name=(String)updatenames.get(un);
 907                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
 908                 } else {
 909                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 910                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 911                     if (usageimage)
 912                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
 913                     if (usageinvimage)
 914                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
 915                     UpdateNode un=munadd.getUpdate(0);
 916                     String name=(String)updatenames.get(un);
 917                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
 918                 }
 919             } else {
 920                 SetDescriptor sd=(SetDescriptor)d;
 921                 if (sources.setSource(sd)) {
 922                     /* Set Source */
 923                     /* Set Source */
 924                     SetDescriptor sourcesd=sources.getSourceSet(sd);
 925                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
 926                     cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
 927                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
 928                     cr.startblock();
 929                     cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
 930                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
 931                     cr.outputline(iterator.getSafeSymbol()+"->next();");
 932                     cr.endblock();
 933                 } else if (sources.allocSource(sd)) {
 934                     /* Allocation Source*/
 935                     sources.generateSourceAlloc(cr,newobject,sd);
 936                 } else throw new Error("No source for adding to Set");
 937                 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
 938                 UpdateNode un=munadd.getUpdate(0);
 939                 String name=(String)updatenames.get(un);
 940                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
 941             }
 942             cr.endblock();
 943         }
 944     }
 945
 946     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 947         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
 948         boolean negated=dpred.isNegated();
 949         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
 950         VarDescriptor leftvar=VarDescriptor.makeNew("left");
 951         ip.expr.generate(cr, leftvar);
 952
 953         if (negated) {
 954             if (ip.setexpr instanceof ImageSetExpr) {
 955                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
 956                 VarDescriptor rightvar=ise.getVar();
 957                 boolean inverse=ise.inverted();
 958                 RelationDescriptor rd=ise.getRelation();
 959                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 960                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 961                 if (inverse) {
 962                     if (usageimage)
 963                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 964                     if (usageinvimage)
 965                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 966                 } else {
 967                     if (usageimage)
 968                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 969                     if (usageinvimage)
 970                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 971                 }
 972                 for(int i=0;i<state.vRules.size();i++) {
 973                     Rule r=(Rule)state.vRules.get(i);
 974                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 975                         for(int j=0;j<mun.numUpdates();j++) {
 976                             UpdateNode un=mun.getUpdate(i);
 977                             if (un.getRule()==r) {
 978                                 /* Update for rule rule r */
 979                                 String name=(String)updatenames.get(un);
 980                                 if (inverse) {
 981                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
 982                                 } else {
 983                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
 984                                 }
 985                             }
 986                         }
 987                     }
 988                 }
 989             } else {
 990                 SetDescriptor sd=ip.setexpr.sd;
 991                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
 992
 993                 for(int i=0;i<state.vRules.size();i++) {
 994                     Rule r=(Rule)state.vRules.get(i);
 995                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
 996                         for(int j=0;j<mun.numUpdates();j++) {
 997                             UpdateNode un=mun.getUpdate(i);
 998                             if (un.getRule()==r) {
 999                                 /* Update for rule rule r */
1000                                 String name=(String)updatenames.get(un);
1001                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1002                             }
1003                         }
1004                     }
1005                 }
1006             }
1007         } else {
1008             /* Generate update */
1009             if (ip.setexpr instanceof ImageSetExpr) {
1010                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1011                 VarDescriptor rightvar=ise.getVar();
1012                 boolean inverse=ise.inverted();
1013                 RelationDescriptor rd=ise.getRelation();
1014                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1015                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1016                 if (inverse) {
1017                     if (usageimage)
1018                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
1019                     if (usageinvimage)
1020                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
1021                 } else {
1022                     if (usageimage)
1023                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1024                     if (usageinvimage)
1025                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1026                 }
1027                 UpdateNode un=mun.getUpdate(0);
1028                 String name=(String)updatenames.get(un);
1029                 if (inverse) {
1030                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1031                 } else {
1032                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1033                 }
1034             } else {
1035                 SetDescriptor sd=ip.setexpr.sd;
1036                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
1037
1038                 UpdateNode un=mun.getUpdate(0);
1039                 /* Update for rule rule r */
1040                 String name=(String)updatenames.get(un);
1041                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1042             }
1043         }
1044     }
1045
1046
1047
1048     public static Vector getrulelist(Descriptor d) {
1049         Vector dispatchrules = new Vector();
1050         Vector rules = State.currentState.vRules;
1051
1052         for (int i = 0; i < rules.size(); i++) {
1053             Rule rule = (Rule) rules.elementAt(i);
1054             Set requiredsymbols = rule.getRequiredDescriptors();
1055
1056             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1057             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1058             // fashion...
1059
1060             if (rule.getRequiredDescriptors().contains(d)) {
1061                 dispatchrules.addElement(rule);
1062             }
1063         }
1064         return dispatchrules;
1065     }
1066
1067     private boolean need_compensation(Rule r) {
1068         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1069         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1070             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1071             GraphNode gn2=edge.getTarget();
1072             if (!removed.contains(gn2)) {
1073                 TermNode tn2=(TermNode)gn2.getOwner();
1074                 if (tn2.getType()==TermNode.CONSEQUENCE)
1075                     return false;
1076             }
1077         }
1078         return true;
1079     }
1080
1081     private UpdateNode find_compensation(Rule r) {
1082         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1083         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1084             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1085             GraphNode gn2=edge.getTarget();
1086             if (!removed.contains(gn2)) {
1087                 TermNode tn2=(TermNode)gn2.getOwner();
1088                 if (tn2.getType()==TermNode.UPDATE) {
1089                     MultUpdateNode mun=tn2.getUpdate();
1090                     for(int i=0;i<mun.numUpdates();i++) {
1091                         UpdateNode un=mun.getUpdate(i);
1092                         if (un.getRule()==r)
1093                             return un;
1094                     }
1095                 }
1096             }
1097         }
1098         throw new Error("No Compensation Update could be found");
1099     }
1100
1101     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1102         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1103         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1104
1105         if (!(usageinvimage||usageimage)) /* not used at all*/
1106             return;
1107
1108         cr.outputline("// RELATION DISPATCH ");
1109         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1110         if (usageimage)
1111             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1112         else
1113             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1114         cr.startblock(); {
1115             /* Adding new item */
1116             /* Perform safety checks */
1117             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1118             cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1119             cr.startblock(); {
1120                 /* Have update to call into */
1121                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1122                 String parttype="";
1123                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1124                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1125                         parttype=parttype+", int, int";
1126                     else
1127                         parttype=parttype+", int";
1128                 }
1129                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1130                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1131                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1132                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1133                     Quantifier q=currentrule.getQuantifier(i);
1134                     if (q instanceof SetQuantifier) {
1135                         SetQuantifier sq=(SetQuantifier) q;
1136                         methodcall+=","+sq.getVar().getSafeSymbol();
1137                     } else if (q instanceof RelationQuantifier) {
1138                         RelationQuantifier rq=(RelationQuantifier) q;
1139                         methodcall+=","+rq.x.getSafeSymbol();
1140                         methodcall+=","+rq.y.getSafeSymbol();
1141                     } else if (q instanceof ForQuantifier) {
1142                         ForQuantifier fq=(ForQuantifier) q;
1143                         methodcall+=","+fq.getVar().getSafeSymbol();
1144                     }
1145                 }
1146                 methodcall+=");";
1147                 cr.outputline(methodcall);
1148                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1149                 cr.outputline("continue;");
1150             }
1151             cr.endblock();
1152             /* Build standard compensation actions */
1153             if (need_compensation(currentrule)) {
1154                 UpdateNode un=find_compensation(currentrule);
1155                 String name=(String)updatenames.get(un);
1156                 usedupdates.add(un); /* Mark as used */
1157                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1158                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1159                     Quantifier q=currentrule.getQuantifier(i);
1160                     if (q instanceof SetQuantifier) {
1161                         SetQuantifier sq=(SetQuantifier) q;
1162                         methodcall+=","+sq.getVar().getSafeSymbol();
1163                     } else if (q instanceof RelationQuantifier) {
1164                         RelationQuantifier rq=(RelationQuantifier) q;
1165                         methodcall+=","+rq.x.getSafeSymbol();
1166                         methodcall+=","+rq.y.getSafeSymbol();
1167                     } else if (q instanceof ForQuantifier) {
1168                         ForQuantifier fq=(ForQuantifier) q;
1169                         methodcall+=","+fq.getVar().getSafeSymbol();
1170                     }
1171                 }
1172                 methodcall+=");";
1173                 cr.outputline(methodcall);
1174                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1175                 cr.outputline("continue;");
1176             }
1177         }
1178         cr.endblock();
1179
1180         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1181         cr.outputline("int " + addeditem + ";");
1182         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1183             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1184         }
1185
1186         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1187             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1188         }
1189
1190         cr.outputline("if (" + addeditem + ")");
1191         cr.startblock();
1192
1193         Vector dispatchrules = getrulelist(rd);
1194
1195         if (dispatchrules.size() == 0) {
1196             cr.outputline("// nothing to dispatch");
1197             cr.endblock();
1198             return;
1199         }
1200
1201         for(int i = 0; i < dispatchrules.size(); i++) {
1202             Rule rule = (Rule) dispatchrules.elementAt(i);
1203             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1204                 /* Guard depends on this relation, so we recomput everything */
1205                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1206             } else {
1207                 for (int j=0;j<rule.numQuantifiers();j++) {
1208                     Quantifier q=rule.getQuantifier(j);
1209                     if (q.getRequiredDescriptors().contains(rd)) {
1210                         /* Generate add */
1211                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1212                     }
1213                 }
1214             }
1215         }
1216         cr.endblock();
1217     }
1218
1219
1220     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1221
1222         cr.outputline("// SET DISPATCH ");
1223
1224         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1225         cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1226         cr.startblock(); {
1227             /* Adding new item */
1228             /* Perform safety checks */
1229             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1230             cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1231             cr.startblock(); {
1232                 /* Have update to call into */
1233                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1234                 String parttype="";
1235                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1236                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1237                         parttype=parttype+", int, int";
1238                     else
1239                         parttype=parttype+", int";
1240                 }
1241                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1242                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1243                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1244                               repairtable.getSafeSymbol();
1245                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1246                     Quantifier q=currentrule.getQuantifier(i);
1247                     if (q instanceof SetQuantifier) {
1248                         SetQuantifier sq=(SetQuantifier) q;
1249                         methodcall+=","+sq.getVar().getSafeSymbol();
1250                     } else if (q instanceof RelationQuantifier) {
1251                         RelationQuantifier rq=(RelationQuantifier) q;
1252                         methodcall+=","+rq.x.getSafeSymbol();
1253                         methodcall+=","+rq.y.getSafeSymbol();
1254                     } else if (q instanceof ForQuantifier) {
1255                         ForQuantifier fq=(ForQuantifier) q;
1256                         methodcall+=","+fq.getVar().getSafeSymbol();
1257                     }
1258                 }
1259                 methodcall+=");";
1260                 cr.outputline(methodcall);
1261                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1262                 cr.outputline("continue;");
1263             }
1264             cr.endblock();
1265             /* Build standard compensation actions */
1266             if (need_compensation(currentrule)) {
1267                 UpdateNode un=find_compensation(currentrule);
1268                 String name=(String)updatenames.get(un);
1269                 usedupdates.add(un); /* Mark as used */
1270
1271                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1272                               repairtable.getSafeSymbol();
1273                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1274                     Quantifier q=currentrule.getQuantifier(i);
1275                     if (q instanceof SetQuantifier) {
1276                         SetQuantifier sq=(SetQuantifier) q;
1277                         methodcall+=","+sq.getVar().getSafeSymbol();
1278                     } else if (q instanceof RelationQuantifier) {
1279                         RelationQuantifier rq=(RelationQuantifier) q;
1280                         methodcall+=","+rq.x.getSafeSymbol();
1281                         methodcall+=","+rq.y.getSafeSymbol();
1282                     } else if (q instanceof ForQuantifier) {
1283                         ForQuantifier fq=(ForQuantifier) q;
1284                         methodcall+=","+fq.getVar().getSafeSymbol();
1285                     }
1286                 }
1287                 methodcall+=");";
1288                 cr.outputline(methodcall);
1289                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1290                 cr.outputline("continue;");
1291             }
1292         }
1293         cr.endblock();
1294
1295         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1296         cr.outputline("int " + addeditem + " = 1;");
1297         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1298         cr.startblock();
1299         Vector dispatchrules = getrulelist(sd);
1300
1301         if (dispatchrules.size() == 0) {
1302             cr.outputline("// nothing to dispatch");
1303             cr.endblock();
1304             return;
1305         }
1306
1307         for(int i = 0; i < dispatchrules.size(); i++) {
1308             Rule rule = (Rule) dispatchrules.elementAt(i);
1309             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1310                 /* Guard depends on this relation, so we recompute everything */
1311                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1312             } else {
1313                 for (int j=0;j<rule.numQuantifiers();j++) {
1314                     Quantifier q=rule.getQuantifier(j);
1315                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1316                         /* Generate add */
1317                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1318                     }
1319                 }
1320             }
1321         }
1322         cr.endblock();
1323     }
1324 }
1325
1326
1327