KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > graph > SFSReduction


1
2 //
3 // Copyright (C) 2005 United States Government as represented by the
4 // Administrator of the National Aeronautics and Space Administration
5 // (NASA). All Rights Reserved.
6 //
7 // This software is distributed under the NASA Open Source Agreement
8 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
9 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
10 // directory tree for the complete NOSA document.
11 //
12 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
13 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
14 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
15 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
16 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
17 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
18 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
19 //
20 package gov.nasa.ltl.graph;
21
22 import java.io.*;
23
24 import java.util.Iterator JavaDoc;
25 import java.util.LinkedList JavaDoc;
26 import java.util.List JavaDoc;
27 import java.util.StringTokenizer JavaDoc;
28 import java.util.TreeSet JavaDoc;
29 import java.util.Vector JavaDoc;
30
31
32 /**
33  * DOCUMENT ME!
34  */
35 public class SFSReduction {
36   public static void main (String JavaDoc[] args) {
37     if (args.length > 1) {
38       System.out.println("usage:");
39       System.out.println("\tjava gov.nasa.ltl.graph.SFSReduction [<filename>]");
40
41       return;
42     }
43
44     Graph g = null;
45
46     try {
47       if (args.length == 0) {
48         g = Graph.load();
49       } else {
50         g = Graph.load(args[0]);
51       }
52     } catch (IOException e) {
53       System.out.println("Can't load the graph.");
54
55       return;
56     }
57
58     Graph reduced = reduce(g);
59
60     reduced.save();
61   }
62
63   public static Graph reduce (Graph g) {
64     // debugged by Dimitra 3/4/02 - added |PO| information so that main while
65 // loop works correctly - removed break statement based on color only
66 int currNumColors;
67     int prevNumColors = 1;
68     int currNumPO = 3;
69     int prevNumPO = 1;
70     TreeSet JavaDoc newColorSet = null;
71     LinkedList JavaDoc newColorList = null;
72     boolean accepting = false;
73     boolean nonaccepting = false;
74
75     // Initialization
76 List JavaDoc nodes = g.getNodes();
77
78     for (Iterator JavaDoc i = nodes.iterator(); i.hasNext();) {
79       Node currNode = (Node) i.next();
80       currNode.setIntAttribute("_prevColor", 1);
81
82       if (isAccepting(currNode)) {
83         currNode.setIntAttribute("_currColor", 1);
84         accepting = true;
85       } else {
86         currNode.setIntAttribute("_currColor", 2);
87         nonaccepting = true;
88       }
89     }
90
91     if (accepting && nonaccepting) {
92       currNumColors = 2;
93     } else {
94       currNumColors = 1;
95     }
96
97     // po(i, j)
98 boolean[][] currPO = new boolean[2][2];
99     boolean[][] prevPO;
100
101     for (int i = 0; i < 2; i++) {
102       for (int j = 0; j < 2; j++) {
103         if (i >= j) {
104           currPO[i][j] = true;
105         } else {
106           currPO[i][j] = false;
107         }
108       }
109     }
110
111     while ((currNumColors != prevNumColors) || (currNumPO != prevNumPO)) {
112       // Incrementing i, equiv. current values become previous ones
113 for (Iterator JavaDoc i = nodes.iterator(); i.hasNext();) {
114         Node currNode = (Node) i.next();
115         currNode.setIntAttribute("_prevColor",
116                                  currNode.getIntAttribute("_currColor"));
117       }
118
119       prevPO = currPO;
120       prevNumColors = currNumColors;
121
122
123       // Getting the new color pairs
124 newColorList = new LinkedList JavaDoc(); // keeps association of node with new color
125 newColorSet = new TreeSet JavaDoc(); // keeps set of new colors
126
127       for (Iterator JavaDoc i = nodes.iterator(); i.hasNext();) {
128         Node currNode = (Node) i.next();
129
130         ColorPair currPair = new ColorPair(currNode.getIntAttribute(
131                                                  "_prevColor"),
132                                            getPrevN(currNode, prevPO));
133
134
135         /* System.out.println("Transition set from node: " + currNode.getId()
136            + " is: " + currPair.getIMaxSet());
137          */
138         newColorList.add(new Pair(currNode.getId(), currPair));
139         newColorSet.add(currPair);
140       }
141
142       currNumColors = newColorSet.size();
143
144       // System.out.println("The number of colors is: " + currNumColors + "\n");
145 // Dimitra comments
146 // Convert the set into a linked list so that rank of object is known
147 // originally used set to avoid duplicates
148 // rank will just be the position of the object in the list
149 LinkedList JavaDoc ordered = new LinkedList JavaDoc();
150
151       for (Iterator JavaDoc i = newColorSet.iterator(); i.hasNext();) {
152         ColorPair currPair = (ColorPair) i.next();
153         ordered.add(currPair);
154       }
155
156       // Renaming color set
157 for (Iterator JavaDoc i = newColorList.iterator(); i.hasNext();) {
158         Pair cPair = (Pair) i.next();
159         ColorPair currPair = (ColorPair) cPair.getElement();
160         g.getNode(cPair.getValue())
161          .setIntAttribute("_currColor", ordered.indexOf(currPair) + 1);
162       }
163
164
165       // Update partial order
166 prevNumPO = currNumPO;
167       currNumPO = 0;
168       currPO = new boolean[currNumColors][currNumColors];
169
170       for (Iterator JavaDoc i = newColorList.iterator(); i.hasNext();) {
171         ColorPair currPairOne = (ColorPair) ((Pair) i.next()).getElement();
172
173         for (Iterator JavaDoc j = newColorList.iterator(); j.hasNext();) {
174           ColorPair currPairTwo = (ColorPair) ((Pair) j.next()).getElement();
175           boolean po = prevPO[currPairTwo.getColor() - 1][currPairOne.getColor() - 1];
176           boolean dominate = iDominateSet(currPairOne.getIMaxSet(),
177                                             currPairTwo.getIMaxSet(), prevPO);
178
179           if (po && dominate) {
180             currPO[ordered.indexOf(currPairTwo)][ordered.indexOf(currPairOne)] = true;
181             currNumPO++;
182           } else {
183             currPO[ordered.indexOf(currPairTwo)][ordered.indexOf(currPairOne)] = false;
184           }
185         }
186       }
187     }
188
189     // Create new graph
190 Graph result;
191
192     if (newColorList == null) {
193       result = g;
194     } else {
195       result = new Graph();
196
197       Node[] newNodes = new Node[currNumColors];
198
199       for (int i = 0; i < currNumColors; i++) {
200         Node n = new Node(result);
201         newNodes[i] = n;
202       }
203
204       for (Iterator JavaDoc i = newColorList.iterator(); i.hasNext();) {
205         Pair nodePair = (Pair) i.next();
206         int origNodeId = nodePair.getValue();
207         ColorPair colPair = (ColorPair) nodePair.getElement();
208
209         if (newColorSet.contains(colPair)) {
210           // for all transitions based on colors, newColorSet makes sure that
211 // no duplicates exist, neither transitions that dominate each other
212 // that is why we only add transitions that belong to it;
213 // I guess we could also just use all transitions in newColorSet to
214 // create the new transition relation
215 newColorSet.remove(colPair);
216
217           TreeSet JavaDoc pairSet = (TreeSet JavaDoc) colPair.getIMaxSet();
218           int color = colPair.getColor();
219           Node currNode = newNodes[color - 1];
220
221           for (Iterator JavaDoc j = pairSet.iterator(); j.hasNext();) {
222             ITypeNeighbor neigh = (ITypeNeighbor) j.next();
223             int neighPos = neigh.getColor() - 1;
224             Edge currEdge = new Edge(currNode, newNodes[neighPos],
225                                               neigh.getTransition());
226           }
227
228           // starting node
229 if (g.getInit().getId() == origNodeId) {
230             result.setInit(currNode);
231           }
232
233           // accepting node
234 if (isAccepting(g.getNode(origNodeId))) {
235             currNode.setBooleanAttribute("accepting", true);
236           }
237         } else {
238         } // ignore such transitions
239 }
240     }
241
242     return reachabilityGraph(result);
243
244     //return result;
245 }
246
247   private static boolean isAccepting (Node nodeIn) {
248     return (nodeIn.getBooleanAttribute("accepting"));
249   }
250
251   private static TreeSet JavaDoc getPrevN (Node currNode, boolean[][] prevPO) {
252     List JavaDoc edges = currNode.getOutgoingEdges();
253     LinkedList JavaDoc neighbors = new LinkedList JavaDoc();
254     ITypeNeighbor iNeigh;
255     TreeSet JavaDoc prevN = new TreeSet JavaDoc();
256
257     for (Iterator JavaDoc i = edges.iterator(); i.hasNext();) {
258       Edge currEdge = (Edge) i.next();
259       iNeigh = new ITypeNeighbor(currEdge.getNext()
260                                          .getIntAttribute("_prevColor"),
261                                  currEdge.getGuard());
262       neighbors.add(iNeigh);
263     }
264
265     // No neighbors present
266 if (neighbors.size() == 0) {
267       return prevN;
268     }
269
270     // Get the first of the list. Remove it from the list. Compare
271 // this element with the rest of the list. If element subsumes
272 // something in remainder of list remove that thing from list. If
273 // element is subsumed, throw element away, else put element in
274 // set
275 boolean useless;
276
277     do {
278       useless = false;
279       iNeigh = (ITypeNeighbor) neighbors.removeFirst();
280
281       for (Iterator JavaDoc i = neighbors.iterator(); i.hasNext();) {
282         ITypeNeighbor nNeigh = (ITypeNeighbor) i.next();
283         ITypeNeighbor dominating = iDominates(iNeigh, nNeigh, prevPO);
284
285         if (dominating == iNeigh) {
286           i.remove();
287         }
288
289         if (dominating == nNeigh) {
290           useless = true;
291
292           break;
293         }
294       }
295
296       if (!useless) {
297         prevN.add(iNeigh);
298       }
299     } while (neighbors.size() > 0);
300
301     return prevN;
302   }
303
304   private static boolean iDominateSet (TreeSet JavaDoc setOne, TreeSet JavaDoc setTwo,
305                                        boolean[][] prevPO) {
306     TreeSet JavaDoc working = new TreeSet JavaDoc(setTwo);
307
308     for (Iterator JavaDoc i = working.iterator(); i.hasNext();) {
309       ITypeNeighbor neighTwo = (ITypeNeighbor) i.next();
310
311       for (Iterator JavaDoc j = setOne.iterator(); j.hasNext();) {
312         ITypeNeighbor neighOne = (ITypeNeighbor) j.next();
313         ITypeNeighbor dominating = iDominates(neighOne, neighTwo, prevPO);
314
315         if (dominating == neighOne) {
316           i.remove();
317
318           break;
319         }
320       }
321     }
322
323     if (working.size() == 0) {
324       return true;
325     }
326
327     return false;
328   }
329
330   /** Returns the neighbor that dominates. If none dominates the
331    * other, then returns null
332    */
333   private static ITypeNeighbor iDominates (ITypeNeighbor iNeigh,
334                                            ITypeNeighbor nNeigh,
335                                            boolean[][] prevPO) {
336     String JavaDoc iTerm = iNeigh.getTransition();
337     String JavaDoc nTerm = nNeigh.getTransition();
338     int iColor = iNeigh.getColor();
339     int nColor = nNeigh.getColor();
340     String JavaDoc theSubterm = subterm(iTerm, nTerm);
341
342     if (theSubterm == iTerm) {
343       if (prevPO[nColor - 1][iColor - 1]) {
344         // iNeigh i-dominates nNeigh
345 return iNeigh;
346       } else {
347         return null;
348       }
349     }
350
351     if (theSubterm == nTerm) {
352       if (prevPO[iColor - 1][nColor - 1]) {
353         // nNeigh i-dominates iNeigh
354 return nNeigh;
355       } else {
356         return null;
357       }
358     }
359
360     if (theSubterm.equals("true")) {
361       if (prevPO[nColor - 1][iColor - 1]) {
362         // iNeigh i-dominates nNeigh
363 return iNeigh;
364       } else if (prevPO[iColor - 1][nColor - 1]) {
365         // nNeigh i-dominates iNeigh
366 return nNeigh;
367       }
368     }
369
370     return null;
371   }
372
373   private static Graph reachabilityGraph (Graph g) {
374     Vector JavaDoc work = new Vector JavaDoc();
375     Vector JavaDoc reachable = new Vector JavaDoc();
376     work.add(g.getInit());
377
378     while (!work.isEmpty()) {
379       Node currNode = (Node) work.firstElement();
380       reachable.add(currNode);
381
382       if (currNode != null) {
383         List JavaDoc outgoingEdges = currNode.getOutgoingEdges();
384
385         for (Iterator JavaDoc i = outgoingEdges.iterator(); i.hasNext();) {
386           Edge currEdge = (Edge) i.next();
387           Node nextNode = (Node) currEdge.getNext();
388
389           if (!(work.contains(nextNode) || reachable.contains(nextNode))) {
390             work.add(nextNode);
391           }
392         }
393       }
394
395       if (work.remove(0) != currNode) {
396         System.out.println("ERROR"); // should probably throw exception
397 }
398     }
399
400     List JavaDoc nodes = g.getNodes();
401
402     if (nodes != null) {
403       for (Iterator JavaDoc i = nodes.iterator(); i.hasNext();) {
404         Node n = (Node) i.next();
405
406         if (!reachable.contains(n)) {
407           g.removeNode(n);
408         }
409       }
410     }
411
412     return g;
413   }
414
415   private static String JavaDoc subterm (String JavaDoc pred1, String JavaDoc pred2) {
416     if (pred1.equals("-") && pred2.equals("-")) {
417       return "true";
418     }
419
420     if (pred1.equals("-")) {
421       return pred1;
422     }
423
424     if (pred2.equals("-")) {
425       return pred2;
426     }
427
428     if ((pred1.indexOf("true") != -1) && (pred2.indexOf("true") != -1)) {
429       return "true";
430     }
431
432     if (pred1.indexOf("true") != -1) {
433       return pred1;
434     }
435
436     if (pred2.indexOf("true") != -1) {
437       return pred2;
438     }
439
440     // ASSUMPTION: the shortest predicate, i.e. with less litterals,
441 // will most probably be the subterm of the other predicate
442 // (provided terms are simplified)
443 // alpha subterm of tau, i.e. tau implies alpha
444 String JavaDoc alphaStr;
445     String JavaDoc tauStr;
446
447     if (pred1.length() <= pred2.length()) {
448       alphaStr = pred1;
449       tauStr = pred2;
450     } else {
451       alphaStr = pred2;
452       tauStr = pred1;
453     }
454
455     StringTokenizer JavaDoc alphaTk = new StringTokenizer JavaDoc(alphaStr, "&");
456     StringTokenizer JavaDoc tauTk = new StringTokenizer JavaDoc(tauStr, "&");
457     LinkedList JavaDoc tauLst = new LinkedList JavaDoc();
458
459     // Putting the litterals of tau in a list - for easier access
460 while (tauTk.hasMoreTokens()) {
461       String JavaDoc token = tauTk.nextToken();
462       tauLst.add(token);
463     }
464
465     while (alphaTk.hasMoreTokens()) {
466       String JavaDoc alphaLit = alphaTk.nextToken();
467
468       if (!tauLst.contains(alphaLit)) {
469         return "false";
470       }
471     }
472
473     if (pred1.length() == pred2.length()) {
474       return "true";
475     }
476
477     return alphaStr;
478   }
479 }
Popular Tags