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