5 public class GraphAnalysis {
6 Termination termination;
7 static final int WORKS=0;
8 static final int ERR_NOREPAIR=1;
9 static final int ERR_CYCLE=2;
10 static final int ERR_RULE=3;
11 static final int ERR_ABSTRACT=4;
13 public GraphAnalysis(Termination t) {
17 public Set doAnalysis() {
18 HashSet cantremove=new HashSet();
19 HashSet mustremove=new HashSet();
20 HashSet optionalabstractrepair=new HashSet();
22 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
23 GraphNode gn=(GraphNode)it.next();
24 TermNode tn=(TermNode)gn.getOwner();
25 AbstractRepair ar=tn.getAbstract();
26 DNFPredicate dpred=ar.getPredicate();
27 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
28 if ((repairnodes.size()>1)&&
29 containsmodify(repairnodes)) {
30 optionalabstractrepair.add(gn);
34 cantremove.addAll(termination.scopenodes);
35 cantremove.addAll(termination.abstractrepair);
36 cantremove.removeAll(optionalabstractrepair);
40 HashSet nodes=new HashSet();
41 nodes.addAll(termination.conjunctions);
42 nodes.removeAll(mustremove);
43 GraphNode.computeclosure(nodes,mustremove);
44 Set cycles=GraphNode.findcycles(nodes);
45 Set couldremove=new HashSet();
46 couldremove.addAll(termination.conjunctions);
47 couldremove.addAll(termination.updatenodes);
48 couldremove.addAll(termination.consequencenodes);
49 couldremove.addAll(optionalabstractrepair);
50 couldremove.retainAll(cycles);
53 /* Look for constraints which can only be satisfied one way */
55 Vector constraints=termination.state.vConstraints;
56 for(int i=0;i<constraints.size();i++) {
57 Constraint c=(Constraint)constraints.get(i);
58 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
59 HashSet tmpset=new HashSet();
60 tmpset.addAll(conjunctionset);
61 tmpset.removeAll(mustremove);
62 if (tmpset.size()==1) {
63 int oldsize=cantremove.size();
64 cantremove.addAll(tmpset);
65 if (cantremove.size()!=oldsize)
70 /* Search through conjunction which must be satisfied, and attempt
71 to generate appropriate repair actions
73 HashSet newset=new HashSet();
74 for(Iterator cit=cantremove.iterator();cit.hasNext();) {
75 GraphNode gn=(GraphNode)cit.next();
76 boolean nomodify=true;
77 HashSet toremove=new HashSet();
78 if (termination.conjunctions.contains(gn)) {
79 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
80 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
81 GraphNode gn2=e.getTarget();
82 TermNode tn2=(TermNode)gn2.getOwner();
83 if (nodes.contains(gn2)&&!mustremove.contains(gn2)&&
84 tn2.getType()==TermNode.ABSTRACT) {
86 HashSet updateset=new HashSet();
87 for(Iterator upit=gn2.edges();upit.hasNext();) {
88 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
89 GraphNode gn3=e2.getTarget();
90 TermNode tn3=(TermNode)gn3.getOwner();
91 if (tn3.getType()==TermNode.UPDATE)
94 updateset.removeAll(mustremove);
96 AbstractRepair ar=tn2.getAbstract();
97 DNFPredicate dpred=ar.getPredicate();
98 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
99 if (repairnodes.size()>1&&
100 containsmodify(repairnodes)) {
101 /* We are modifying a relation */
102 HashSet retainednodes=new HashSet();
103 retainednodes.addAll(repairnodes);
104 retainednodes.retainAll(nodes);
106 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
107 if (updateset.size()==0) {
108 if (retainednodes.size()>1) {
111 } else return null; /* Out of luck */
113 if (updateset.size()==1&&retainednodes.size()==1)
114 toremove.addAll(updateset); /* Required update */
116 /* Addition or removal to relation */
117 assert (ar.getType()==AbstractRepair.ADDTORELATION)||(ar.getType()==AbstractRepair.REMOVEFROMRELATION);
118 if (updateset.size()==0) {
119 if (containsmodify(retainednodes)) {
120 /* Both ADD & REMOVE are no good */
121 for(Iterator it=retainednodes.iterator();it.hasNext();) {
122 GraphNode gnit=(GraphNode)it.next();
123 TermNode tnit=(TermNode)gnit.getOwner();
124 AbstractRepair arit=tnit.getAbstract();
125 if (arit.getType()!=AbstractRepair.MODIFYRELATION) {
126 mustremove.add(gnit);
131 return null; /* Out of luck */
133 if (updateset.size()==1&&retainednodes.size()==2)
134 toremove.addAll(updateset); /* Required update */
136 } else if (updateset.size()==1)
137 toremove.addAll(updateset);
140 newset.addAll(toremove);
144 int oldsize=cantremove.size();
145 cantremove.addAll(newset);
146 if (cantremove.size()!=oldsize)
150 /* Look for required actions for scope nodes */
151 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
152 GraphNode gn=(GraphNode)scopeit.next();
153 HashSet tmpset=new HashSet();
154 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
155 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
156 tmpset.add(e.getTarget());
158 tmpset.removeAll(mustremove);
159 if (tmpset.size()==1) {
160 int oldsize=cantremove.size();
161 cantremove.addAll(tmpset);
162 if (cantremove.size()!=oldsize)
167 Set cycles2=GraphNode.findcycles(cantremove);
168 for(Iterator it=cycles2.iterator();it.hasNext();) {
169 GraphNode gn=(GraphNode)it.next();
170 if (termination.conjunctions.contains(gn))
171 return null; // Out of luck
175 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
176 GraphNode gn=(GraphNode)it.next();
177 boolean foundnocycle=false;
179 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
180 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
181 GraphNode gn2=e.getTarget();
182 TermNode tn2=(TermNode)gn2.getOwner();
183 if (tn2.getType()!=TermNode.ABSTRACT)
185 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
186 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
187 GraphNode gn3=e2.getTarget();
188 TermNode tn3=(TermNode)gn3.getOwner();
189 if (tn3.getType()!=TermNode.UPDATE)
191 boolean containsgn=cantremove.contains(gn);
192 boolean containsgn3=cantremove.contains(gn3);
195 Set cycle=GraphNode.findcycles(cantremove);
196 if (cycle.contains(gn3)) {
197 if (!mustremove.contains(gn3)) {
202 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
206 cantremove.remove(gn);
208 cantremove.remove(gn3);
212 if (!mustremove.contains(gn)) {
218 couldremove.removeAll(mustremove);
219 couldremove.removeAll(cantremove);
221 Vector couldremovevector=new Vector();
222 couldremovevector.addAll(couldremove);
223 Vector combination=new Vector();
225 continue; //recalculate
227 System.out.println("Searching set of "+couldremove.size()+" nodes.");
228 System.out.println("Eliminated must "+mustremove.size()+" nodes");
229 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
230 System.out.println("Searching following set:");
231 for(Iterator it=couldremove.iterator();it.hasNext();) {
232 GraphNode gn=(GraphNode)it.next();
233 System.out.println(gn.getTextLabel());
238 if (illegal(combination,couldremovevector))
240 Set combinationset=buildset(combination,couldremovevector);
241 checkmodify(combinationset);
242 combinationset.addAll(mustremove);
243 if (combinationset!=null) {
244 System.out.println("Checkabstract="+checkAbstract(combinationset));
245 System.out.println("Checkrepairs="+checkRepairs(combinationset));
246 System.out.println("Checkall="+checkAll(combinationset));
248 if (checkAbstract(combinationset)==0&&
249 checkRepairs(combinationset)==0&&
250 checkAll(combinationset)==0) {
251 return combinationset;
254 increment(combination,couldremovevector);
260 private void checkmodify(Set removednodes) {
261 for (Iterator it=removednodes.iterator();it.hasNext();) {
262 GraphNode gn=(GraphNode)it.next();
263 TermNode tn=(TermNode)gn.getOwner();
264 if (tn.getType()==TermNode.ABSTRACT) {
265 AbstractRepair ar=tn.getAbstract();
266 DNFPredicate dpred=ar.getPredicate();
267 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
268 /* Has MODIFYRELATION */
269 if (containsmodify(repairnodes)&&
270 (repairnodes.size()>1)&&
271 (ar.getType()==AbstractRepair.REMOVEFROMRELATION||
272 ar.getType()==AbstractRepair.ADDTORELATION)) {
273 for(Iterator it2=repairnodes.iterator();it2.hasNext();) {
274 GraphNode gn2=(GraphNode)it2.next();
275 TermNode tn2=(TermNode)gn2.getOwner();
276 AbstractRepair ar2=tn2.getAbstract();
277 if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION||
278 ar2.getType()==AbstractRepair.ADDTORELATION) {
279 removednodes.add(gn2);
287 private static boolean containsmodify(Set repairnodes) {
288 for (Iterator it=repairnodes.iterator();it.hasNext();) {
289 GraphNode gn=(GraphNode) it.next();
290 TermNode tn=(TermNode)gn.getOwner();
291 AbstractRepair ar=tn.getAbstract();
292 if (ar.getType()==AbstractRepair.MODIFYRELATION)
298 private static Set buildset(Vector combination, Vector couldremove) {
300 for(int i=0;i<combination.size();i++) {
301 int index=((Integer)combination.get(i)).intValue();
302 Object o=couldremove.get(index);
311 private static boolean illegal(Vector combination, Vector couldremove) {
312 if (combination.size()>couldremove.size())
316 private static void increment(Vector combination, Vector couldremove) {
317 boolean incremented=false;
318 boolean forcereset=false;
319 for(int i=0;i<combination.size();i++) {
320 int newindex=((Integer)combination.get(i)).intValue()+1;
321 if (newindex==couldremove.size()||forcereset) {
323 if ((i+1)==combination.size()) {
326 newindex=((Integer)combination.get(i+1)).intValue()+2;
327 for(int j=i;j>=0;j--) {
328 combination.set(j,new Integer(newindex));
331 if (newindex>couldremove.size())
335 combination.set(i,new Integer(newindex));
339 if (incremented==false) /* Increase length */ {
340 combination.add(new Integer(0));
341 System.out.println("Expanding to :"+combination.size());
345 /* This function checks the graph as a whole for bad cycles */
346 public int checkAll(Collection removed) {
347 Set nodes=new HashSet();
348 nodes.addAll(termination.conjunctions);
349 nodes.removeAll(removed);
350 GraphNode.computeclosure(nodes,removed);
351 Set cycles=GraphNode.findcycles(nodes);
352 for(Iterator it=cycles.iterator();it.hasNext();) {
353 GraphNode gn=(GraphNode)it.next();
354 TermNode tn=(TermNode)gn.getOwner();
355 switch(tn.getType()) {
356 case TermNode.UPDATE:
357 case TermNode.CONJUNCTION:
359 case TermNode.ABSTRACT:
360 case TermNode.RULESCOPE:
361 case TermNode.CONSEQUENCE:
369 /* This function checks that
370 1) All abstract repairs have a corresponding data structure update
372 2) All scope nodes have either a consequence node or a compensation
373 node that isn't removed.
375 public int checkRepairs(Collection removed) {
376 Set nodes=new HashSet();
377 nodes.addAll(termination.conjunctions);
378 nodes.removeAll(removed);
379 GraphNode.computeclosure(nodes,removed);
380 Set toretain=new HashSet();
381 toretain.addAll(termination.abstractrepair);
382 toretain.addAll(termination.scopenodes);
383 nodes.retainAll(toretain);
384 /* Nodes is now the reachable set of abstractrepairs */
385 /* Check to see that each has an implementation */
386 for(Iterator it=nodes.iterator();it.hasNext();) {
387 GraphNode gn=(GraphNode)it.next();
388 TermNode tn=(TermNode)gn.getOwner();
389 if (tn.getType()==TermNode.RULESCOPE) {
390 boolean foundnode=false;
391 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
392 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
393 GraphNode gn2=edge.getTarget();
394 if (!removed.contains(gn2)) {
395 TermNode tn2=(TermNode)gn2.getOwner();
396 if ((tn2.getType()==TermNode.CONSEQUENCE)||
397 (tn2.getType()==TermNode.UPDATE)) {
404 System.out.println(gn.getTextLabel());
407 } else if (tn.getType()==TermNode.ABSTRACT) {
408 boolean foundnode=false;
409 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
410 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
411 GraphNode gn2=edge.getTarget();
412 if (!removed.contains(gn2)) {
413 TermNode tn2=(TermNode)gn2.getOwner();
414 if (tn2.getType()==TermNode.UPDATE) {
422 } else throw new Error("Unanticipated Node");
426 /* This method checks that all constraints have conjunction nodes
427 and that there are no bad cycles in the abstract portion of the graph.
429 public int checkAbstract(Collection removed) {
430 Vector constraints=termination.state.vConstraints;
431 for(int i=0;i<constraints.size();i++) {
432 Constraint c=(Constraint)constraints.get(i);
433 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
435 boolean foundrepair=false;
436 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
437 GraphNode gn=(GraphNode)it.next();
438 if (!removed.contains(gn)) {
440 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
441 GraphNode.Edge edge=(GraphNode.Edge) edgeit.next();
442 GraphNode gn2=edge.getTarget();
443 TermNode tn2=(TermNode) gn2.getOwner();
444 if (tn2.getType()==TermNode.ABSTRACT) {
446 AbstractRepair ar=tn2.getAbstract();
447 DNFPredicate dpred=ar.getPredicate();
448 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
449 if (containsmodify(repairnodes)&&
450 (repairnodes.size()>1)) {
451 HashSet retainednodes=new HashSet();
452 retainednodes.addAll(repairnodes);
453 retainednodes.removeAll(removed);
454 if (!containsmodify(retainednodes)&&
455 (retainednodes.size()<2))
457 } else if (removed.contains(gn2))
466 Set abstractnodes=new HashSet();
467 abstractnodes.addAll(termination.conjunctions);
468 abstractnodes.removeAll(removed);
469 GraphNode.computeclosure(abstractnodes,removed);
471 Set tset=new HashSet();
472 tset.addAll(termination.conjunctions);
473 tset.addAll(termination.abstractrepair);
474 tset.addAll(termination.scopenodes);
475 tset.addAll(termination.consequencenodes);
476 abstractnodes.retainAll(tset);
477 Set cycles=GraphNode.findcycles(abstractnodes);
479 for(Iterator it=cycles.iterator();it.hasNext();) {
480 GraphNode gn=(GraphNode)it.next();
481 System.out.println("NODE: "+gn.getTextLabel());
482 TermNode tn=(TermNode)gn.getOwner();
483 switch(tn.getType()) {
484 case TermNode.CONJUNCTION:
485 case TermNode.ABSTRACT:
487 case TermNode.UPDATE:
488 throw new Error("No Update Nodes should be here");