7 public class Termination {
9 Hashtable conjunctionmap;
11 HashSet abstractrepair;
12 HashSet abstractrepairadd;
15 HashSet consequencenodes;
18 Hashtable scopesatisfy;
19 Hashtable scopefalsify;
20 Hashtable consequence;
21 Hashtable abstractadd;
22 Hashtable abstractremove;
23 Hashtable conjtonodemap;
24 Hashtable predtoabstractmap;
26 ComputeMaxSize maxsize;
28 AbstractInterferes abstractinterferes;
31 public Termination(State state) {
33 conjunctions=new HashSet();
34 conjunctionmap=new Hashtable();
35 abstractrepair=new HashSet();
36 abstractrepairadd=new HashSet();
37 scopenodes=new HashSet();
38 scopesatisfy=new Hashtable();
39 scopefalsify=new Hashtable();
40 consequence=new Hashtable();
41 updatenodes=new HashSet();
42 consequencenodes=new HashSet();
43 abstractadd=new Hashtable();
44 abstractremove=new Hashtable();
45 conjtonodemap=new Hashtable();
46 predtoabstractmap=new Hashtable();
51 for(int i=0;i<state.vRules.size();i++)
52 System.out.println(state.vRules.get(i));
53 for(int i=0;i<state.vConstraints.size();i++)
54 System.out.println(state.vConstraints.get(i));
57 maxsize=new ComputeMaxSize(state);
59 abstractinterferes=new AbstractInterferes(this);
60 generateconjunctionnodes();
62 generaterepairnodes();
63 generatedatastructureupdatenodes();
64 generatecompensationnodes();
66 generateabstractedges();
68 generateupdateedges();
70 HashSet superset=new HashSet();
71 superset.addAll(conjunctions);
72 HashSet closureset=new HashSet();
73 // closureset.addAll(updatenodes);
74 //superset.addAll(abstractrepair);
75 //superset.addAll(updatenodes);
76 //superset.addAll(scopenodes);
77 //superset.addAll(consequencenodes);
78 GraphNode.computeclosure(superset,closureset);
80 GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
81 } catch (Exception e) {
85 for(Iterator it=updatenodes.iterator();it.hasNext();) {
86 GraphNode gn=(GraphNode)it.next();
87 TermNode tn=(TermNode)gn.getOwner();
88 MultUpdateNode mun=tn.getUpdate();
89 System.out.println(gn.getTextLabel());
90 System.out.println(mun.toString());
92 GraphAnalysis ga=new GraphAnalysis(this);
93 removedset=ga.doAnalysis();
94 if (removedset==null) {
95 System.out.println("Can't generate terminating repair algorithm!");
98 System.out.println("Removing:");
99 for(Iterator it=removedset.iterator();it.hasNext();) {
100 GraphNode gn=(GraphNode)it.next();
101 System.out.println(gn.getTextLabel());
104 superset=new HashSet();
105 superset.addAll(conjunctions);
106 superset.removeAll(removedset);
107 GraphNode.computeclosure(superset,removedset);
109 GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
110 } catch (Exception e) {
118 /** This method generates a node for each conjunction in the DNF form of each constraint.
119 * It also converts the quantifiers into conjunctions also - constraints can be satisfied by
120 * removing items from the sets and relations they are quantified over */
121 void generateconjunctionnodes() {
122 Vector constraints=state.vConstraints;
123 // Constructs conjunction nodes
124 for(int i=0;i<constraints.size();i++) {
125 Constraint c=(Constraint)constraints.get(i);
126 DNFConstraint dnf=c.dnfconstraint;
127 for(int j=0;j<dnf.size();j++) {
128 TermNode tn=new TermNode(c,dnf.get(j));
129 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
130 "Conj ("+i+","+j+") "+dnf.get(j).name()
132 conjunctions.add(gn);
133 if (!conjunctionmap.containsKey(c))
134 conjunctionmap.put(c,new HashSet());
135 ((Set)conjunctionmap.get(c)).add(gn);
136 conjtonodemap.put(dnf.get(j),gn);
138 // Construct quantifier "conjunction" nodes
139 for(int j=0;j<c.numQuantifiers();j++) {
140 Quantifier q=c.getQuantifier(j);
141 if (q instanceof SetQuantifier) {
142 SetQuantifier sq=(SetQuantifier)q;
143 VarExpr ve=new VarExpr(sq.getVar());
144 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
145 DNFConstraint dconst=new DNFConstraint(ip);
147 TermNode tn=new TermNode(c,dconst.get(0));
148 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
149 "Conj ("+i+","+j+") "+dconst.get(0).name()
151 conjunctions.add(gn);
152 if (!conjunctionmap.containsKey(c))
153 conjunctionmap.put(c,new HashSet());
154 ((Set)conjunctionmap.get(c)).add(gn);
155 conjtonodemap.put(dconst.get(0),gn);
156 } else if (q instanceof RelationQuantifier) {
157 RelationQuantifier rq=(RelationQuantifier)q;
158 VarExpr ve=new VarExpr(rq.y);
159 InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
160 DNFConstraint dconst=new DNFConstraint(ip);
162 TermNode tn=new TermNode(c,dconst.get(0));
163 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
164 "Conj ("+i+","+j+") "+dconst.get(0).name()
166 conjunctions.add(gn);
167 if (!conjunctionmap.containsKey(c))
168 conjunctionmap.put(c,new HashSet());
169 ((Set)conjunctionmap.get(c)).add(gn);
170 conjtonodemap.put(dconst.get(0),gn);
176 void generateupdateedges() {
177 for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
178 GraphNode gn=(GraphNode)updateiterator.next();
179 TermNode tn=(TermNode)gn.getOwner();
180 MultUpdateNode mun=tn.getUpdate();
181 /* Cycle through the rules to look for possible conflicts */
182 for(int i=0;i<state.vRules.size();i++) {
183 Rule r=(Rule) state.vRules.get(i);
184 if (ConcreteInterferes.interferes(mun,r,true)) {
185 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
186 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
189 if (ConcreteInterferes.interferes(mun,r,false)) {
190 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
191 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
198 void generateabstractedges() {
199 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
200 GraphNode gn=(GraphNode)absiterator.next();
201 TermNode tn=(TermNode)gn.getOwner();
202 AbstractRepair ar=(AbstractRepair)tn.getAbstract();
204 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
205 GraphNode gn2=(GraphNode)conjiterator.next();
206 TermNode tn2=(TermNode)gn2.getOwner();
207 Conjunction conj=tn2.getConjunction();
208 Constraint cons=tn2.getConstraint();
210 for(int i=0;i<conj.size();i++) {
211 DNFPredicate dp=conj.get(i);
212 if (AbstractInterferes.interferes(ar,cons)||
213 abstractinterferes.interferes(ar,dp)) {
214 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
221 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
222 GraphNode gn2=(GraphNode)scopeiterator.next();
223 TermNode tn2=(TermNode)gn2.getOwner();
224 ScopeNode sn2=tn2.getScope();
225 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
226 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
233 void generatescopeedges() {
234 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
235 GraphNode gn=(GraphNode)scopeiterator.next();
236 TermNode tn=(TermNode)gn.getOwner();
237 ScopeNode sn=tn.getScope();
239 /* Interference edges with conjunctions */
240 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
241 GraphNode gn2=(GraphNode)conjiterator.next();
242 TermNode tn2=(TermNode)gn2.getOwner();
243 Conjunction conj=tn2.getConjunction();
244 Constraint constr=tn2.getConstraint();
245 for(int i=0;i<conj.size();i++) {
246 DNFPredicate dp=conj.get(i);
247 if (abstractinterferes.interferes(sn,dp)||
248 AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
249 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
250 GraphNode gnconseq=(GraphNode)consequence.get(sn);
257 /* Now see if this could effect other model defintion rules */
258 for(int i=0;i<state.vRules.size();i++) {
259 Rule r=(Rule) state.vRules.get(i);
260 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
261 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
262 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
263 GraphNode gnconseq=(GraphNode)consequence.get(sn);
266 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
267 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
268 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
269 GraphNode gnconseq=(GraphNode)consequence.get(sn);
276 /** This method generates the abstract repair nodes. */
277 void generaterepairnodes() {
278 /* Generate repairs of conjunctions */
279 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
280 GraphNode gn=(GraphNode)conjiterator.next();
281 TermNode tn=(TermNode)gn.getOwner();
282 Conjunction conj=tn.getConjunction();
283 for(int i=0;i<conj.size();i++) {
284 DNFPredicate dp=conj.get(i);
285 int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
286 Descriptor d=dp.getPredicate().getDescriptor();
287 for(int j=0;j<array.length;j++) {
288 AbstractRepair ar=new AbstractRepair(dp,array[j],d);
289 TermNode tn2=new TermNode(ar);
290 GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
291 GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
293 if (!predtoabstractmap.containsKey(dp))
294 predtoabstractmap.put(dp,new HashSet());
295 ((Set)predtoabstractmap.get(dp)).add(gn2);
296 abstractrepair.add(gn2);
300 /* Generate additional abstract repairs */
301 Vector setdescriptors=state.stSets.getAllDescriptors();
302 for(int i=0;i<setdescriptors.size();i++) {
303 SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
305 /* XXXXXXX: Not sure what to do here */
306 VarExpr ve=new VarExpr("DUMMY");
307 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
309 DNFPredicate tp=new DNFPredicate(false,ip);
310 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
311 TermNode tn=new TermNode(ar);
312 GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
313 if (!predtoabstractmap.containsKey(tp))
314 predtoabstractmap.put(tp,new HashSet());
315 ((Set)predtoabstractmap.get(tp)).add(gn);
316 abstractrepair.add(gn);
317 abstractrepairadd.add(gn);
318 abstractadd.put(sd,gn);
320 DNFPredicate tp2=new DNFPredicate(true,ip);
321 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
322 TermNode tn2=new TermNode(ar2);
323 GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
324 if (!predtoabstractmap.containsKey(tp2))
325 predtoabstractmap.put(tp2,new HashSet());
326 ((Set)predtoabstractmap.get(tp2)).add(gn2);
327 abstractrepair.add(gn2);
328 abstractrepairadd.add(gn2);
329 abstractremove.put(sd,gn2);
332 Vector relationdescriptors=state.stRelations.getAllDescriptors();
333 for(int i=0;i<relationdescriptors.size();i++) {
334 RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
336 /* XXXXXXX: Not sure what to do here */
337 VarDescriptor vd1=new VarDescriptor("DUMMY1");
338 VarExpr ve2=new VarExpr("DUMMY2");
340 InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
342 DNFPredicate tp=new DNFPredicate(false,ip);
343 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
344 TermNode tn=new TermNode(ar);
345 GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
346 if (!predtoabstractmap.containsKey(tp))
347 predtoabstractmap.put(tp,new HashSet());
348 ((Set)predtoabstractmap.get(tp)).add(gn);
349 abstractrepair.add(gn);
350 abstractrepairadd.add(gn);
351 abstractadd.put(rd,gn);
353 DNFPredicate tp2=new DNFPredicate(true,ip);
354 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
355 TermNode tn2=new TermNode(ar2);
356 GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
357 if (!predtoabstractmap.containsKey(tp2))
358 predtoabstractmap.put(tp2,new HashSet());
359 ((Set)predtoabstractmap.get(tp2)).add(gn2);
360 abstractrepair.add(gn2);
361 abstractrepairadd.add(gn2);
362 abstractremove.put(rd,gn2);
367 int compensationcount=0;
368 void generatecompensationnodes() {
369 for(int i=0;i<state.vRules.size();i++) {
370 Rule r=(Rule) state.vRules.get(i);
371 Vector possiblerules=new Vector();
372 /* Construct bindings */
373 /* No need to construct bindings on remove
374 Vector bindings=new Vector();
375 constructbindings(bindings, r,true);
377 for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
378 GraphNode gn=(GraphNode)scopesatisfy.get(r);
379 TermNode tn=(TermNode) gn.getOwner();
380 ScopeNode sn=tn.getScope();
381 MultUpdateNode mun=new MultUpdateNode(sn);
382 TermNode tn2=new TermNode(mun);
383 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
384 UpdateNode un=new UpdateNode(r);
385 // un.addBindings(bindings);
387 if (j<r.numQuantifiers()) {
388 /* Remove quantifier */
389 Quantifier q=r.getQuantifier(j);
390 if (q instanceof RelationQuantifier) {
391 RelationQuantifier rq=(RelationQuantifier)q;
392 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
393 toe.td=ReservedTypeDescriptor.INT;
394 Updates u=new Updates(toe,true);
396 if (abstractremove.containsKey(rq.relation)) {
397 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
398 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
401 continue; /* Abstract repair doesn't exist */
403 } else if (q instanceof SetQuantifier) {
404 SetQuantifier sq=(SetQuantifier)q;
405 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
406 eoe.td=ReservedTypeDescriptor.INT;
407 Updates u=new Updates(eoe,true);
409 if (abstractremove.containsKey(sq.set)) {
410 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
411 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
414 continue; /* Abstract repair doesn't exist */
420 int c=j-r.numQuantifiers();
421 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
425 if (!un.checkupdates()) /* Make sure we have a good update */
430 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
433 updatenodes.add(gn2);
438 void generatedatastructureupdatenodes() {
439 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
440 GraphNode gn=(GraphNode)absiterator.next();
441 TermNode tn=(TermNode) gn.getOwner();
442 AbstractRepair ar=tn.getAbstract();
443 if (ar.getType()==AbstractRepair.ADDTOSET) {
444 generateaddtosetrelation(gn,ar);
445 } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
446 generateremovefromsetrelation(gn,ar);
447 } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
448 generateaddtosetrelation(gn,ar);
449 } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
450 generateremovefromsetrelation(gn,ar);
451 } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
452 /* Generate remove/add pairs */
453 generateremovefromsetrelation(gn,ar);
454 generateaddtosetrelation(gn,ar);
455 /* Generate atomic modify */
456 generatemodifyrelation(gn,ar);
461 int removefromcount=0;
462 void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
463 Vector possiblerules=new Vector();
464 for(int i=0;i<state.vRules.size();i++) {
465 Rule r=(Rule) state.vRules.get(i);
466 if ((r.getInclusion() instanceof SetInclusion)&&
467 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
468 possiblerules.add(r);
469 if ((r.getInclusion() instanceof RelationInclusion)&&
470 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
471 possiblerules.add(r);
473 if (possiblerules.size()==0)
475 int[] count=new int[possiblerules.size()];
476 while(remains(count,possiblerules,true)) {
477 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
478 TermNode tn=new TermNode(mun);
479 GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
481 boolean goodflag=true;
482 for(int i=0;i<possiblerules.size();i++) {
483 Rule r=(Rule)possiblerules.get(i);
484 UpdateNode un=new UpdateNode(r);
485 /* Construct bindings */
486 /* No Need to construct bindings on remove
487 Vector bindings=new Vector();
488 constructbindings(bindings, r,true);
489 un.addBindings(bindings);*/
490 if (count[i]<r.numQuantifiers()) {
491 /* Remove quantifier */
492 Quantifier q=r.getQuantifier(count[i]);
493 if (q instanceof RelationQuantifier) {
494 RelationQuantifier rq=(RelationQuantifier)q;
495 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
496 toe.td=ReservedTypeDescriptor.INT;
497 Updates u=new Updates(toe,true);
499 if (abstractremove.containsKey(rq.relation)) {
500 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
501 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
504 goodflag=false;break; /* Abstract repair doesn't exist */
506 } else if (q instanceof SetQuantifier) {
507 SetQuantifier sq=(SetQuantifier)q;
508 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
509 eoe.td=ReservedTypeDescriptor.INT;
510 Updates u=new Updates(eoe,true);
512 if (abstractremove.containsKey(sq.set)) {
513 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
514 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
517 goodflag=false;break; /* Abstract repair doesn't exist */
519 } else {goodflag=false;break;}
521 int c=count[i]-r.numQuantifiers();
522 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
523 goodflag=false;break;
526 if (!un.checkupdates()) {
533 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
536 updatenodes.add(gn2);
538 increment(count,possiblerules,true);
542 static private void increment(int count[], Vector rules,boolean isremove) {
544 for(int i=0;i<(rules.size()-1);i++) {
545 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
553 static private boolean remains(int count[], Vector rules, boolean isremove) {
554 for(int i=0;i<rules.size();i++) {
555 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
563 /** This method generates data structure updates to implement the
564 * abstract atomic modification specified by ar. */
566 void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
567 RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
568 ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
569 boolean inverted=exprPredicate.inverted();
578 Vector possiblerules=new Vector();
579 for(int i=0;i<state.vRules.size();i++) {
580 Rule r=(Rule) state.vRules.get(i);
581 if ((r.getInclusion() instanceof RelationInclusion)&&
582 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
583 possiblerules.add(r);
585 if (possiblerules.size()==0)
587 int[] count=new int[possiblerules.size()];
588 while(remains(count,possiblerules,false)) {
589 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
590 TermNode tn=new TermNode(mun);
591 GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
593 boolean goodflag=true;
594 for(int i=0;i<possiblerules.size();i++) {
595 Rule r=(Rule)possiblerules.get(i);
596 UpdateNode un=new UpdateNode(r);
597 /* No Need to construct bindings on modify */
600 if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
601 goodflag=false;break;
603 RelationInclusion ri=(RelationInclusion)r.getInclusion();
604 if (!(ri.getLeftExpr() instanceof VarExpr)) {
605 if (ri.getLeftExpr().isValue()) {
606 Updates up=new Updates(ri.getLeftExpr(),leftindex);
611 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
613 Updates up=new Updates(ri.getLeftExpr(),leftindex);
618 if (!(ri.getRightExpr() instanceof VarExpr)) {
619 if (ri.getRightExpr().isValue()) {
620 Updates up=new Updates(ri.getRightExpr(),rightindex);
625 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
627 Updates up=new Updates(ri.getRightExpr(),rightindex);
629 } else if (!inverted)
633 if (!un.checkupdates()) {
640 GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
643 updatenodes.add(gn2);
645 increment(count,possiblerules,false);
648 /** This method constructs bindings for an update using rule
649 * r. The boolean flag isremoval indicates that the update
650 * performs a removal. The function returns true if it is able to
651 * generate a valid set of bindings and false otherwise. */
653 boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
654 boolean goodupdate=true;
655 Inclusion inc=r.getInclusion();
656 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
657 Quantifier q=(Quantifier)iterator.next();
658 if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
659 VarDescriptor vd=null;
660 SetDescriptor set=null;
661 if (q instanceof SetQuantifier) {
662 vd=((SetQuantifier)q).getVar();
663 set=((SetQuantifier)q).getSet();
665 vd=((ForQuantifier)q).getVar();
667 if(inc instanceof SetInclusion) {
668 SetInclusion si=(SetInclusion)inc;
669 if ((si.elementexpr instanceof VarExpr)&&
670 (((VarExpr)si.elementexpr).getVar()==vd)) {
671 /* Can solve for v */
672 Binding binding=new Binding(vd,0);
673 bindings.add(binding);
677 } else if (inc instanceof RelationInclusion) {
678 RelationInclusion ri=(RelationInclusion)inc;
681 if ((ri.getLeftExpr() instanceof VarExpr)&&
682 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
683 /* Can solve for v */
684 Binding binding=new Binding(vd,0);
685 bindings.add(binding);
687 if ((ri.getRightExpr() instanceof VarExpr)&&
688 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
689 /* Can solve for v */
690 Binding binding=new Binding(vd,0);
691 bindings.add(binding);
695 } else throw new Error("Inclusion not recognized");
698 /* Removals don't need bindings anymore
699 Binding binding=new Binding(vd);
700 bindings.add(binding);*/
703 /* Create new element to bind to */
704 Binding binding=new Binding(vd,set,createorsearch(set));
705 bindings.add(binding);
709 } else if (q instanceof RelationQuantifier) {
710 RelationQuantifier rq=(RelationQuantifier)q;
711 for(int k=0;k<2;k++) {
712 VarDescriptor vd=(k==0)?rq.x:rq.y;
713 if(inc instanceof SetInclusion) {
714 SetInclusion si=(SetInclusion)inc;
715 if ((si.elementexpr instanceof VarExpr)&&
716 (((VarExpr)si.elementexpr).getVar()==vd)) {
717 /* Can solve for v */
718 Binding binding=new Binding(vd,0);
719 bindings.add(binding);
722 } else if (inc instanceof RelationInclusion) {
723 RelationInclusion ri=(RelationInclusion)inc;
726 if ((ri.getLeftExpr() instanceof VarExpr)&&
727 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
728 /* Can solve for v */
729 Binding binding=new Binding(vd,0);
730 bindings.add(binding);
732 if ((ri.getRightExpr() instanceof VarExpr)&&
733 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
734 /* Can solve for v */
735 Binding binding=new Binding(vd,0);
736 bindings.add(binding);
740 } else throw new Error("Inclusion not recognized");
743 /* Removals don't need bindings anymore
744 Binding binding=new Binding(vd);
745 bindings.add(binding);*/
752 } else throw new Error("Quantifier not recognized");
757 /** Returns true if we search for an element from sd
758 * false if we create an element for sd */
759 private boolean createorsearch(SetDescriptor sd) {
763 static int addtocount=0;
764 void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
765 for(int i=0;i<state.vRules.size();i++) {
766 Rule r=(Rule) state.vRules.get(i);
767 /* See if this is a good rule*/
768 if ((r.getInclusion() instanceof SetInclusion&&
769 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
770 (r.getInclusion() instanceof RelationInclusion&&
771 ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
773 /* First solve for quantifiers */
774 Vector bindings=new Vector();
775 /* Construct bindings */
776 if (!constructbindings(bindings,r,false))
778 //Generate add instruction
779 DNFRule dnfrule=r.getDNFGuardExpr();
780 for(int j=0;j<dnfrule.size();j++) {
781 Inclusion inc=r.getInclusion();
782 UpdateNode un=new UpdateNode(r);
783 un.addBindings(bindings);
784 /* Now build update for tuple/set inclusion condition */
785 if(inc instanceof SetInclusion) {
786 SetInclusion si=(SetInclusion)inc;
787 if (!(si.elementexpr instanceof VarExpr)) {
788 if (si.elementexpr.isValue()) {
789 Updates up=new Updates(si.elementexpr,0);
794 VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
796 Updates up=new Updates(si.elementexpr,0);
800 } else if (inc instanceof RelationInclusion) {
801 RelationInclusion ri=(RelationInclusion)inc;
802 if (!(ri.getLeftExpr() instanceof VarExpr)) {
803 if (ri.getLeftExpr().isValue()) {
804 Updates up=new Updates(ri.getLeftExpr(),0);
809 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
811 Updates up=new Updates(ri.getLeftExpr(),0);
815 if (!(ri.getRightExpr() instanceof VarExpr)) {
816 if (ri.getRightExpr().isValue()) {
817 Updates up=new Updates(ri.getRightExpr(),1);
822 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
824 Updates up=new Updates(ri.getRightExpr(),1);
829 //Finally build necessary updates to satisfy conjunction
830 RuleConjunction ruleconj=dnfrule.get(j);
832 /* Add in updates for quantifiers */
833 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
834 TermNode tn=new TermNode(mun);
835 GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
837 if (processquantifers(gn2,un, r)&&
838 processconjunction(un,ruleconj)&&
841 GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
844 updatenodes.add(gn2);}
850 /** Adds updates that add an item to the appropriate set or
851 * relation quantified over by the model definition rule.. */
853 boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
854 Inclusion inc=r.getInclusion();
855 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
856 Quantifier q=(Quantifier)iterator.next();
858 /* FIXME: Analysis to determine when this update is necessary */
859 if (q instanceof RelationQuantifier) {
860 RelationQuantifier rq=(RelationQuantifier)q;
861 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
862 toe.td=ReservedTypeDescriptor.INT;
863 Updates u=new Updates(toe,false);
865 if (abstractremove.containsKey(rq.relation)) {
866 GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
867 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
873 } else if (q instanceof SetQuantifier) {
874 SetQuantifier sq=(SetQuantifier)q;
875 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
876 eoe.td=ReservedTypeDescriptor.INT;
877 Updates u=new Updates(eoe,false);
879 if (abstractremove.containsKey(sq.set)) {
880 GraphNode agn=(GraphNode)abstractadd.get(sq.set);
881 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
891 boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){
893 for(int k=0;k<ruleconj.size();k++) {
894 DNFExpr de=ruleconj.get(k);
896 if (e instanceof OpExpr) {
897 OpExpr ex=(OpExpr)de.getExpr();
898 Opcode op=ex.getOpcode();
899 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
901 } else if (e instanceof ElementOfExpr) {
902 Updates up=new Updates(e,de.getNegation());
904 } else if (e instanceof TupleOfExpr) {
905 Updates up=new Updates(e,de.getNegation());
907 } else if (e instanceof BooleanLiteralExpr) {
908 boolean truth=((BooleanLiteralExpr)e).getValue();
909 if (de.getNegation())
916 System.out.println(e.getClass().getName());
917 throw new Error("Unrecognized Expr");
923 void generatescopenodes() {
924 for(int i=0;i<state.vRules.size();i++) {
925 Rule r=(Rule) state.vRules.get(i);
926 ScopeNode satisfy=new ScopeNode(r,true);
927 TermNode tnsatisfy=new TermNode(satisfy);
928 GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
929 ConsequenceNode cnsatisfy=new ConsequenceNode();
930 TermNode ctnsatisfy=new TermNode(cnsatisfy);
931 GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
932 consequence.put(satisfy,cgnsatisfy);
933 GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
934 gnsatisfy.addEdge(esat);
935 consequencenodes.add(cgnsatisfy);
936 scopesatisfy.put(r,gnsatisfy);
937 scopenodes.add(gnsatisfy);
939 ScopeNode falsify=new ScopeNode(r,false);
940 TermNode tnfalsify=new TermNode(falsify);
941 GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
942 ConsequenceNode cnfalsify=new ConsequenceNode();
943 TermNode ctnfalsify=new TermNode(cnfalsify);
944 GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
945 consequence.put(falsify,cgnfalsify);
946 GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
947 gnfalsify.addEdge(efals);
948 consequencenodes.add(cgnfalsify);
949 scopefalsify.put(r,gnfalsify);
950 scopenodes.add(gnfalsify);