7 public class Termination {
9 Hashtable conjunctionmap;
11 HashSet abstractrepair;
13 HashSet consequencenodes;
16 Hashtable scopesatisfy;
17 Hashtable scopefalsify;
18 Hashtable consequence;
19 Hashtable abstractadd;
20 Hashtable abstractremove;
21 Hashtable conjtonodemap;
22 Hashtable predtoabstractmap;
27 public Termination(State state) {
29 conjunctions=new HashSet();
30 conjunctionmap=new Hashtable();
31 abstractrepair=new HashSet();
32 scopenodes=new HashSet();
33 scopesatisfy=new Hashtable();
34 scopefalsify=new Hashtable();
35 consequence=new Hashtable();
36 updatenodes=new HashSet();
37 consequencenodes=new HashSet();
38 abstractadd=new Hashtable();
39 abstractremove=new Hashtable();
40 conjtonodemap=new Hashtable();
41 predtoabstractmap=new Hashtable();
45 generateconjunctionnodes();
47 generaterepairnodes();
48 generatedatastructureupdatenodes();
49 generatecompensationnodes();
51 generateabstractedges();
53 generateupdateedges();
55 HashSet superset=new HashSet();
56 superset.addAll(conjunctions);
57 HashSet closureset=new HashSet();
58 // closureset.addAll(updatenodes);
59 //superset.addAll(abstractrepair);
60 //superset.addAll(updatenodes);
61 //superset.addAll(scopenodes);
62 //superset.addAll(consequencenodes);
63 GraphNode.computeclosure(superset,closureset);
65 GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
66 } catch (Exception e) {
70 for(Iterator it=updatenodes.iterator();it.hasNext();) {
71 GraphNode gn=(GraphNode)it.next();
72 TermNode tn=(TermNode)gn.getOwner();
73 MultUpdateNode mun=tn.getUpdate();
74 System.out.println(gn.getTextLabel());
75 System.out.println(mun.toString());
77 GraphAnalysis ga=new GraphAnalysis(this);
78 removedset=ga.doAnalysis();
79 if (removedset==null) {
80 System.out.println("Can't generate terminating repair algorithm!");
83 System.out.println("Removing:");
84 for(Iterator it=removedset.iterator();it.hasNext();) {
85 GraphNode gn=(GraphNode)it.next();
86 System.out.println(gn.getTextLabel());
89 superset=new HashSet();
90 superset.addAll(conjunctions);
91 superset.removeAll(removedset);
92 GraphNode.computeclosure(superset,removedset);
94 GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
95 } catch (Exception e) {
102 void generateconjunctionnodes() {
103 Vector constraints=state.vConstraints;
104 for(int i=0;i<constraints.size();i++) {
105 Constraint c=(Constraint)constraints.get(i);
106 DNFConstraint dnf=c.dnfconstraint;
107 for(int j=0;j<dnf.size();j++) {
108 TermNode tn=new TermNode(c,dnf.get(j));
109 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
110 "Conj ("+i+","+j+") "+dnf.get(j).name()
112 conjunctions.add(gn);
113 if (!conjunctionmap.containsKey(c))
114 conjunctionmap.put(c,new HashSet());
115 ((Set)conjunctionmap.get(c)).add(gn);
116 conjtonodemap.put(dnf.get(j),gn);
118 for(int j=0;j<c.numQuantifiers();j++) {
119 Quantifier q=c.getQuantifier(j);
120 if (q instanceof SetQuantifier) {
121 SetQuantifier sq=(SetQuantifier)q;
122 VarExpr ve=new VarExpr(sq.getVar());
123 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
124 DNFConstraint dconst=new DNFConstraint(ip);
126 TermNode tn=new TermNode(c,dconst.get(0));
127 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
128 "Conj ("+i+","+j+") "+dconst.get(0).name()
130 conjunctions.add(gn);
131 if (!conjunctionmap.containsKey(c))
132 conjunctionmap.put(c,new HashSet());
133 ((Set)conjunctionmap.get(c)).add(gn);
134 conjtonodemap.put(dconst.get(0),gn);
135 } else if (q instanceof RelationQuantifier) {
136 RelationQuantifier rq=(RelationQuantifier)q;
137 VarExpr ve=new VarExpr(rq.y);
138 InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
139 DNFConstraint dconst=new DNFConstraint(ip);
141 TermNode tn=new TermNode(c,dconst.get(0));
142 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
143 "Conj ("+i+","+j+") "+dconst.get(0).name()
145 conjunctions.add(gn);
146 if (!conjunctionmap.containsKey(c))
147 conjunctionmap.put(c,new HashSet());
148 ((Set)conjunctionmap.get(c)).add(gn);
149 conjtonodemap.put(dconst.get(0),gn);
155 void generateupdateedges() {
156 for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
157 GraphNode gn=(GraphNode)updateiterator.next();
158 TermNode tn=(TermNode)gn.getOwner();
159 MultUpdateNode mun=tn.getUpdate();
160 /* Cycle through the rules to look for possible conflicts */
161 for(int i=0;i<state.vRules.size();i++) {
162 Rule r=(Rule) state.vRules.get(i);
163 if (ConcreteInterferes.interferes(mun,r,true)) {
164 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
165 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
168 if (ConcreteInterferes.interferes(mun,r,false)) {
169 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
170 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
177 void generateabstractedges() {
178 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
179 GraphNode gn=(GraphNode)absiterator.next();
180 TermNode tn=(TermNode)gn.getOwner();
181 AbstractRepair ar=(AbstractRepair)tn.getAbstract();
183 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
184 GraphNode gn2=(GraphNode)conjiterator.next();
185 TermNode tn2=(TermNode)gn2.getOwner();
186 Conjunction conj=tn2.getConjunction();
187 Constraint cons=tn2.getConstraint();
189 for(int i=0;i<conj.size();i++) {
190 DNFPredicate dp=conj.get(i);
191 if (AbstractInterferes.interferes(ar,cons)||
192 AbstractInterferes.interferes(ar,dp)) {
193 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
200 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
201 GraphNode gn2=(GraphNode)scopeiterator.next();
202 TermNode tn2=(TermNode)gn2.getOwner();
203 ScopeNode sn2=tn2.getScope();
204 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
205 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
212 void generatescopeedges() {
213 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
214 GraphNode gn=(GraphNode)scopeiterator.next();
215 TermNode tn=(TermNode)gn.getOwner();
216 ScopeNode sn=tn.getScope();
218 /* Interference edges with conjunctions */
219 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
220 GraphNode gn2=(GraphNode)conjiterator.next();
221 TermNode tn2=(TermNode)gn2.getOwner();
222 Conjunction conj=tn2.getConjunction();
223 Constraint constr=tn2.getConstraint();
224 for(int i=0;i<conj.size();i++) {
225 DNFPredicate dp=conj.get(i);
226 if (AbstractInterferes.interferes(sn,dp)||
227 AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
228 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
229 GraphNode gnconseq=(GraphNode)consequence.get(sn);
236 /* Now see if this could effect other model defintion rules */
237 for(int i=0;i<state.vRules.size();i++) {
238 Rule r=(Rule) state.vRules.get(i);
239 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
240 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
241 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
242 GraphNode gnconseq=(GraphNode)consequence.get(sn);
245 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
246 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
247 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
248 GraphNode gnconseq=(GraphNode)consequence.get(sn);
255 /* Generates the abstract repair nodes */
256 void generaterepairnodes() {
257 /* Generate repairs of conjunctions */
258 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
259 GraphNode gn=(GraphNode)conjiterator.next();
260 TermNode tn=(TermNode)gn.getOwner();
261 Conjunction conj=tn.getConjunction();
262 for(int i=0;i<conj.size();i++) {
263 DNFPredicate dp=conj.get(i);
264 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
265 Descriptor d=dp.getPredicate().getDescriptor();
266 for(int j=0;j<array.length;j++) {
267 AbstractRepair ar=new AbstractRepair(dp,array[j],d);
268 TermNode tn2=new TermNode(ar);
269 GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
270 GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
272 if (!predtoabstractmap.containsKey(dp))
273 predtoabstractmap.put(dp,new HashSet());
274 ((Set)predtoabstractmap.get(dp)).add(gn2);
275 abstractrepair.add(gn2);
279 /* Generate additional abstract repairs */
280 Vector setdescriptors=state.stSets.getAllDescriptors();
281 for(int i=0;i<setdescriptors.size();i++) {
282 SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
284 /* XXXXXXX: Not sure what to do here */
285 VarExpr ve=new VarExpr("DUMMY");
286 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
288 DNFPredicate tp=new DNFPredicate(false,ip);
289 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
290 TermNode tn=new TermNode(ar);
291 GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
292 if (!predtoabstractmap.containsKey(tp))
293 predtoabstractmap.put(tp,new HashSet());
294 ((Set)predtoabstractmap.get(tp)).add(gn);
295 abstractrepair.add(gn);
296 abstractadd.put(sd,gn);
298 DNFPredicate tp2=new DNFPredicate(true,ip);
299 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
300 TermNode tn2=new TermNode(ar2);
301 GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
302 if (!predtoabstractmap.containsKey(tp2))
303 predtoabstractmap.put(tp2,new HashSet());
304 ((Set)predtoabstractmap.get(tp2)).add(gn2);
305 abstractrepair.add(gn2);
306 abstractremove.put(sd,gn2);
309 Vector relationdescriptors=state.stRelations.getAllDescriptors();
310 for(int i=0;i<relationdescriptors.size();i++) {
311 RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
313 /* XXXXXXX: Not sure what to do here */
314 VarDescriptor vd1=new VarDescriptor("DUMMY1");
315 VarExpr ve2=new VarExpr("DUMMY2");
317 InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
319 DNFPredicate tp=new DNFPredicate(false,ip);
320 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
321 TermNode tn=new TermNode(ar);
322 GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
323 if (!predtoabstractmap.containsKey(tp))
324 predtoabstractmap.put(tp,new HashSet());
325 ((Set)predtoabstractmap.get(tp)).add(gn);
326 abstractrepair.add(gn);
327 abstractadd.put(rd,gn);
329 DNFPredicate tp2=new DNFPredicate(true,ip);
330 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
331 TermNode tn2=new TermNode(ar2);
332 GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
333 if (!predtoabstractmap.containsKey(tp2))
334 predtoabstractmap.put(tp2,new HashSet());
335 ((Set)predtoabstractmap.get(tp2)).add(gn2);
336 abstractrepair.add(gn2);
337 abstractremove.put(rd,gn2);
342 int compensationcount=0;
343 void generatecompensationnodes() {
344 for(int i=0;i<state.vRules.size();i++) {
345 Rule r=(Rule) state.vRules.get(i);
346 Vector possiblerules=new Vector();
347 /* Construct bindings */
348 /* No need to construct bindings on remove
349 Vector bindings=new Vector();
350 constructbindings(bindings, r,true);
352 for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
353 GraphNode gn=(GraphNode)scopesatisfy.get(r);
354 TermNode tn=(TermNode) gn.getOwner();
355 ScopeNode sn=tn.getScope();
356 MultUpdateNode mun=new MultUpdateNode(sn);
357 TermNode tn2=new TermNode(mun);
358 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
359 UpdateNode un=new UpdateNode(r);
360 // un.addBindings(bindings);
362 if (j<r.numQuantifiers()) {
363 /* Remove quantifier */
364 Quantifier q=r.getQuantifier(j);
365 if (q instanceof RelationQuantifier) {
366 RelationQuantifier rq=(RelationQuantifier)q;
367 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
368 toe.td=ReservedTypeDescriptor.INT;
369 Updates u=new Updates(toe,true);
371 if (abstractremove.containsKey(rq.relation)) {
372 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
373 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
376 continue; /* Abstract repair doesn't exist */
378 } else if (q instanceof SetQuantifier) {
379 SetQuantifier sq=(SetQuantifier)q;
380 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
381 eoe.td=ReservedTypeDescriptor.INT;
382 Updates u=new Updates(eoe,true);
384 if (abstractremove.containsKey(sq.set)) {
385 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
386 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
389 continue; /* Abstract repair doesn't exist */
395 int c=j-r.numQuantifiers();
396 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
400 if (!un.checkupdates()) /* Make sure we have a good update */
405 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
408 updatenodes.add(gn2);
413 void generatedatastructureupdatenodes() {
414 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
415 GraphNode gn=(GraphNode)absiterator.next();
416 TermNode tn=(TermNode) gn.getOwner();
417 AbstractRepair ar=tn.getAbstract();
418 if (ar.getType()==AbstractRepair.ADDTOSET) {
419 generateaddtosetrelation(gn,ar);
420 } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
421 generateremovefromsetrelation(gn,ar);
422 } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
423 generateaddtosetrelation(gn,ar);
424 } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
425 generateremovefromsetrelation(gn,ar);
426 } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
427 /* Generate remove/add pairs */
428 generateremovefromsetrelation(gn,ar);
429 generateaddtosetrelation(gn,ar);
430 /* Generate atomic modify */
431 generatemodifyrelation(gn,ar);
436 int removefromcount=0;
437 void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
438 Vector possiblerules=new Vector();
439 for(int i=0;i<state.vRules.size();i++) {
440 Rule r=(Rule) state.vRules.get(i);
441 if ((r.getInclusion() instanceof SetInclusion)&&
442 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
443 possiblerules.add(r);
444 if ((r.getInclusion() instanceof RelationInclusion)&&
445 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
446 possiblerules.add(r);
448 if (possiblerules.size()==0)
450 int[] count=new int[possiblerules.size()];
451 while(remains(count,possiblerules,true)) {
452 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
453 TermNode tn=new TermNode(mun);
454 GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
456 boolean goodflag=true;
457 for(int i=0;i<possiblerules.size();i++) {
458 Rule r=(Rule)possiblerules.get(i);
459 UpdateNode un=new UpdateNode(r);
460 /* Construct bindings */
461 /* No Need to construct bindings on remove
462 Vector bindings=new Vector();
463 constructbindings(bindings, r,true);
464 un.addBindings(bindings);*/
465 if (count[i]<r.numQuantifiers()) {
466 /* Remove quantifier */
467 Quantifier q=r.getQuantifier(count[i]);
468 if (q instanceof RelationQuantifier) {
469 RelationQuantifier rq=(RelationQuantifier)q;
470 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
471 toe.td=ReservedTypeDescriptor.INT;
472 Updates u=new Updates(toe,true);
474 if (abstractremove.containsKey(rq.relation)) {
475 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
476 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
479 goodflag=false;break; /* Abstract repair doesn't exist */
481 } else if (q instanceof SetQuantifier) {
482 SetQuantifier sq=(SetQuantifier)q;
483 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
484 eoe.td=ReservedTypeDescriptor.INT;
485 Updates u=new Updates(eoe,true);
487 if (abstractremove.containsKey(sq.set)) {
488 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
489 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
492 goodflag=false;break; /* Abstract repair doesn't exist */
494 } else {goodflag=false;break;}
496 int c=count[i]-r.numQuantifiers();
497 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
498 goodflag=false;break;
501 if (!un.checkupdates()) {
508 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
511 updatenodes.add(gn2);
513 increment(count,possiblerules,true);
517 static void increment(int count[], Vector rules,boolean isremove) {
519 for(int i=0;i<(rules.size()-1);i++) {
520 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
528 static boolean remains(int count[], Vector rules, boolean isremove) {
529 for(int i=0;i<rules.size();i++) {
530 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
538 /** This method generates data structure updates to implement the
539 * abstract atomic modification specified by ar. */
541 void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
542 RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
543 ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
544 boolean inverted=exprPredicate.inverted();
553 Vector possiblerules=new Vector();
554 for(int i=0;i<state.vRules.size();i++) {
555 Rule r=(Rule) state.vRules.get(i);
556 if ((r.getInclusion() instanceof RelationInclusion)&&
557 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
558 possiblerules.add(r);
560 if (possiblerules.size()==0)
562 int[] count=new int[possiblerules.size()];
563 while(remains(count,possiblerules,false)) {
564 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
565 TermNode tn=new TermNode(mun);
566 GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
568 boolean goodflag=true;
569 for(int i=0;i<possiblerules.size();i++) {
570 Rule r=(Rule)possiblerules.get(i);
571 UpdateNode un=new UpdateNode(r);
572 /* No Need to construct bindings on modify */
575 if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
576 goodflag=false;break;
578 RelationInclusion ri=(RelationInclusion)r.getInclusion();
579 if (!(ri.getLeftExpr() instanceof VarExpr)) {
580 Updates up=new Updates(ri.getLeftExpr(),leftindex);
583 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
585 Updates up=new Updates(ri.getLeftExpr(),leftindex);
590 if (!(ri.getRightExpr() instanceof VarExpr)) {
591 Updates up=new Updates(ri.getRightExpr(),rightindex);
594 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
596 Updates up=new Updates(ri.getRightExpr(),rightindex);
598 } else if (!inverted)
602 if (!un.checkupdates()) {
609 GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
612 updatenodes.add(gn2);
614 increment(count,possiblerules,false);
619 boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
620 boolean goodupdate=true;
621 Inclusion inc=r.getInclusion();
622 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
623 Quantifier q=(Quantifier)iterator.next();
624 if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
625 VarDescriptor vd=null;
626 SetDescriptor set=null;
627 if (q instanceof SetQuantifier) {
628 vd=((SetQuantifier)q).getVar();
630 vd=((ForQuantifier)q).getVar();
631 if(inc instanceof SetInclusion) {
632 SetInclusion si=(SetInclusion)inc;
633 if ((si.elementexpr instanceof VarExpr)&&
634 (((VarExpr)si.elementexpr).getVar()==vd)) {
635 /* Can solve for v */
636 Binding binding=new Binding(vd,0);
637 bindings.add(binding);
640 } else if (inc instanceof RelationInclusion) {
641 RelationInclusion ri=(RelationInclusion)inc;
644 if ((ri.getLeftExpr() instanceof VarExpr)&&
645 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
646 /* Can solve for v */
647 Binding binding=new Binding(vd,0);
648 bindings.add(binding);
650 if ((ri.getRightExpr() instanceof VarExpr)&&
651 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
652 /* Can solve for v */
653 Binding binding=new Binding(vd,0);
654 bindings.add(binding);
658 } else throw new Error("Inclusion not recognized");
661 Binding binding=new Binding(vd);
662 bindings.add(binding);
666 } else if (q instanceof RelationQuantifier) {
667 RelationQuantifier rq=(RelationQuantifier)q;
668 for(int k=0;k<2;k++) {
669 VarDescriptor vd=(k==0)?rq.x:rq.y;
670 if(inc instanceof SetInclusion) {
671 SetInclusion si=(SetInclusion)inc;
672 if ((si.elementexpr instanceof VarExpr)&&
673 (((VarExpr)si.elementexpr).getVar()==vd)) {
674 /* Can solve for v */
675 Binding binding=new Binding(vd,0);
676 bindings.add(binding);
679 } else if (inc instanceof RelationInclusion) {
680 RelationInclusion ri=(RelationInclusion)inc;
683 if ((ri.getLeftExpr() instanceof VarExpr)&&
684 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
685 /* Can solve for v */
686 Binding binding=new Binding(vd,0);
687 bindings.add(binding);
689 if ((ri.getRightExpr() instanceof VarExpr)&&
690 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
691 /* Can solve for v */
692 Binding binding=new Binding(vd,0);
693 bindings.add(binding);
697 } else throw new Error("Inclusion not recognized");
700 Binding binding=new Binding(vd);
701 bindings.add(binding);
708 } else throw new Error("Quantifier not recognized");
713 static int addtocount=0;
714 void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
715 // System.out.println("Attempting to generate add to set");
716 //System.out.println(ar.getPredicate().getPredicate().name());
717 //System.out.println(ar.getPredicate().isNegated());
718 for(int i=0;i<state.vRules.size();i++) {
719 Rule r=(Rule) state.vRules.get(i);
720 /* See if this is a good rule*/
721 //System.out.println(r.getGuardExpr().name());
722 if ((r.getInclusion() instanceof SetInclusion&&
723 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
724 (r.getInclusion() instanceof RelationInclusion&&
725 ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
727 /* First solve for quantifiers */
728 Vector bindings=new Vector();
729 /* Construct bindings */
730 //System.out.println("Attempting to generate add to set: #2");
731 if (!constructbindings(bindings,r,false))
733 //System.out.println("Attempting to generate add to set: #3");
734 //Generate add instruction
735 DNFRule dnfrule=r.getDNFGuardExpr();
736 for(int j=0;j<dnfrule.size();j++) {
737 Inclusion inc=r.getInclusion();
738 UpdateNode un=new UpdateNode(r);
739 un.addBindings(bindings);
740 /* Now build update for tuple/set inclusion condition */
741 if(inc instanceof SetInclusion) {
742 SetInclusion si=(SetInclusion)inc;
743 if (!(si.elementexpr instanceof VarExpr)) {
744 Updates up=new Updates(si.elementexpr,0);
747 VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
748 if (un.getBinding(vd)==null) {
749 Updates up=new Updates(si.elementexpr,0);
753 } else if (inc instanceof RelationInclusion) {
754 RelationInclusion ri=(RelationInclusion)inc;
755 if (!(ri.getLeftExpr() instanceof VarExpr)) {
756 Updates up=new Updates(ri.getLeftExpr(),0);
759 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
760 if (un.getBinding(vd)==null) {
761 Updates up=new Updates(ri.getLeftExpr(),0);
765 if (!(ri.getRightExpr() instanceof VarExpr)) {
766 Updates up=new Updates(ri.getRightExpr(),1);
769 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
770 if (un.getBinding(vd)==null) {
771 Updates up=new Updates(ri.getRightExpr(),1);
776 //Finally build necessary updates to satisfy conjunction
777 RuleConjunction ruleconj=dnfrule.get(j);
778 /* Add in updates for quantifiers */
779 //System.out.println("Attempting to generate add to set #4");
780 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
781 TermNode tn=new TermNode(mun);
782 GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
784 if (processquantifers(gn2,un, r)&&debugdd()&&
785 processconjunction(un,ruleconj)&&
787 //System.out.println("Attempting to generate add to set #5");
789 GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
792 updatenodes.add(gn2);}
799 //System.out.println("Attempting to generate add to set DD");
803 boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
804 Inclusion inc=r.getInclusion();
805 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
806 Quantifier q=(Quantifier)iterator.next();
808 /* FIXME: Analysis to determine when this update is necessary */
809 if (q instanceof RelationQuantifier) {
810 RelationQuantifier rq=(RelationQuantifier)q;
811 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
812 toe.td=ReservedTypeDescriptor.INT;
813 Updates u=new Updates(toe,false);
815 if (abstractremove.containsKey(rq.relation)) {
816 GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
817 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
823 } else if (q instanceof SetQuantifier) {
824 SetQuantifier sq=(SetQuantifier)q;
825 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
826 eoe.td=ReservedTypeDescriptor.INT;
827 Updates u=new Updates(eoe,false);
829 if (abstractremove.containsKey(sq.set)) {
830 GraphNode agn=(GraphNode)abstractadd.get(sq.set);
831 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
841 boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){
843 for(int k=0;k<ruleconj.size();k++) {
844 DNFExpr de=ruleconj.get(k);
846 if (e instanceof OpExpr) {
847 OpExpr ex=(OpExpr)de.getExpr();
848 Opcode op=ex.getOpcode();
849 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
851 } else if (e instanceof ElementOfExpr) {
852 Updates up=new Updates(e,de.getNegation());
854 } else if (e instanceof TupleOfExpr) {
855 Updates up=new Updates(e,de.getNegation());
857 } else if (e instanceof BooleanLiteralExpr) {
858 boolean truth=((BooleanLiteralExpr)e).getValue();
859 if (de.getNegation())
866 System.out.println(e.getClass().getName());
867 throw new Error("Unrecognized Expr");
873 void generatescopenodes() {
874 for(int i=0;i<state.vRules.size();i++) {
875 Rule r=(Rule) state.vRules.get(i);
876 ScopeNode satisfy=new ScopeNode(r,true);
877 TermNode tnsatisfy=new TermNode(satisfy);
878 GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
879 ConsequenceNode cnsatisfy=new ConsequenceNode();
880 TermNode ctnsatisfy=new TermNode(cnsatisfy);
881 GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
882 consequence.put(satisfy,cgnsatisfy);
883 GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
884 gnsatisfy.addEdge(esat);
885 consequencenodes.add(cgnsatisfy);
886 scopesatisfy.put(r,gnsatisfy);
887 scopenodes.add(gnsatisfy);
889 ScopeNode falsify=new ScopeNode(r,false);
890 TermNode tnfalsify=new TermNode(falsify);
891 GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
892 ConsequenceNode cnfalsify=new ConsequenceNode();
893 TermNode ctnfalsify=new TermNode(cnfalsify);
894 GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
895 consequence.put(falsify,cgnfalsify);
896 GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
897 gnfalsify.addEdge(efals);
898 consequencenodes.add(cgnfalsify);
899 scopefalsify.put(r,gnfalsify);
900 scopenodes.add(gnfalsify);