001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.ltl.graph;
020:
021: import java.io.*;
022:
023: import java.util.Iterator;
024: import java.util.LinkedList;
025: import java.util.List;
026: import java.util.StringTokenizer;
027: import java.util.TreeSet;
028: import java.util.Vector;
029:
030: /**
031: * DOCUMENT ME!
032: */
033: public class SFSReduction {
034: public static void main(String[] args) {
035: if (args.length > 1) {
036: System.out.println("usage:");
037: System.out
038: .println("\tjava gov.nasa.ltl.graph.SFSReduction [<filename>]");
039:
040: return;
041: }
042:
043: Graph g = null;
044:
045: try {
046: if (args.length == 0) {
047: g = Graph.load();
048: } else {
049: g = Graph.load(args[0]);
050: }
051: } catch (IOException e) {
052: System.out.println("Can't load the graph.");
053:
054: return;
055: }
056:
057: Graph reduced = reduce(g);
058:
059: reduced.save();
060: }
061:
062: public static Graph reduce(Graph g) {
063: // debugged by Dimitra 3/4/02 - added |PO| information so that main while
064: // loop works correctly - removed break statement based on color only
065: int currNumColors;
066: int prevNumColors = 1;
067: int currNumPO = 3;
068: int prevNumPO = 1;
069: TreeSet newColorSet = null;
070: LinkedList newColorList = null;
071: boolean accepting = false;
072: boolean nonaccepting = false;
073:
074: // Initialization
075: List nodes = g.getNodes();
076:
077: for (Iterator i = nodes.iterator(); i.hasNext();) {
078: Node currNode = (Node) i.next();
079: currNode.setIntAttribute("_prevColor", 1);
080:
081: if (isAccepting(currNode)) {
082: currNode.setIntAttribute("_currColor", 1);
083: accepting = true;
084: } else {
085: currNode.setIntAttribute("_currColor", 2);
086: nonaccepting = true;
087: }
088: }
089:
090: if (accepting && nonaccepting) {
091: currNumColors = 2;
092: } else {
093: currNumColors = 1;
094: }
095:
096: // po(i, j)
097: boolean[][] currPO = new boolean[2][2];
098: boolean[][] prevPO;
099:
100: for (int i = 0; i < 2; i++) {
101: for (int j = 0; j < 2; j++) {
102: if (i >= j) {
103: currPO[i][j] = true;
104: } else {
105: currPO[i][j] = false;
106: }
107: }
108: }
109:
110: while ((currNumColors != prevNumColors)
111: || (currNumPO != prevNumPO)) {
112: // Incrementing i, equiv. current values become previous ones
113: for (Iterator i = nodes.iterator(); i.hasNext();) {
114: Node currNode = (Node) i.next();
115: currNode.setIntAttribute("_prevColor", currNode
116: .getIntAttribute("_currColor"));
117: }
118:
119: prevPO = currPO;
120: prevNumColors = currNumColors;
121:
122: // Getting the new color pairs
123: newColorList = new LinkedList(); // keeps association of node with new color
124: newColorSet = new TreeSet(); // keeps set of new colors
125:
126: for (Iterator i = nodes.iterator(); i.hasNext();) {
127: Node currNode = (Node) i.next();
128:
129: ColorPair currPair = new ColorPair(currNode
130: .getIntAttribute("_prevColor"), getPrevN(
131: currNode, prevPO));
132:
133: /* System.out.println("Transition set from node: " + currNode.getId()
134: + " is: " + currPair.getIMaxSet());
135: */
136: newColorList.add(new Pair(currNode.getId(), currPair));
137: newColorSet.add(currPair);
138: }
139:
140: currNumColors = newColorSet.size();
141:
142: // System.out.println("The number of colors is: " + currNumColors + "\n");
143: // Dimitra comments
144: // Convert the set into a linked list so that rank of object is known
145: // originally used set to avoid duplicates
146: // rank will just be the position of the object in the list
147: LinkedList ordered = new LinkedList();
148:
149: for (Iterator i = newColorSet.iterator(); i.hasNext();) {
150: ColorPair currPair = (ColorPair) i.next();
151: ordered.add(currPair);
152: }
153:
154: // Renaming color set
155: for (Iterator i = newColorList.iterator(); i.hasNext();) {
156: Pair cPair = (Pair) i.next();
157: ColorPair currPair = (ColorPair) cPair.getElement();
158: g.getNode(cPair.getValue()).setIntAttribute(
159: "_currColor", ordered.indexOf(currPair) + 1);
160: }
161:
162: // Update partial order
163: prevNumPO = currNumPO;
164: currNumPO = 0;
165: currPO = new boolean[currNumColors][currNumColors];
166:
167: for (Iterator i = newColorList.iterator(); i.hasNext();) {
168: ColorPair currPairOne = (ColorPair) ((Pair) i.next())
169: .getElement();
170:
171: for (Iterator j = newColorList.iterator(); j.hasNext();) {
172: ColorPair currPairTwo = (ColorPair) ((Pair) j
173: .next()).getElement();
174: boolean po = prevPO[currPairTwo.getColor() - 1][currPairOne
175: .getColor() - 1];
176: boolean dominate = iDominateSet(currPairOne
177: .getIMaxSet(), currPairTwo.getIMaxSet(),
178: prevPO);
179:
180: if (po && dominate) {
181: currPO[ordered.indexOf(currPairTwo)][ordered
182: .indexOf(currPairOne)] = true;
183: currNumPO++;
184: } else {
185: currPO[ordered.indexOf(currPairTwo)][ordered
186: .indexOf(currPairOne)] = false;
187: }
188: }
189: }
190: }
191:
192: // Create new graph
193: Graph result;
194:
195: if (newColorList == null) {
196: result = g;
197: } else {
198: result = new Graph();
199:
200: Node[] newNodes = new Node[currNumColors];
201:
202: for (int i = 0; i < currNumColors; i++) {
203: Node n = new Node(result);
204: newNodes[i] = n;
205: }
206:
207: for (Iterator i = newColorList.iterator(); i.hasNext();) {
208: Pair nodePair = (Pair) i.next();
209: int origNodeId = nodePair.getValue();
210: ColorPair colPair = (ColorPair) nodePair.getElement();
211:
212: if (newColorSet.contains(colPair)) {
213: // for all transitions based on colors, newColorSet makes sure that
214: // no duplicates exist, neither transitions that dominate each other
215: // that is why we only add transitions that belong to it;
216: // I guess we could also just use all transitions in newColorSet to
217: // create the new transition relation
218: newColorSet.remove(colPair);
219:
220: TreeSet pairSet = (TreeSet) colPair.getIMaxSet();
221: int color = colPair.getColor();
222: Node currNode = newNodes[color - 1];
223:
224: for (Iterator j = pairSet.iterator(); j.hasNext();) {
225: ITypeNeighbor neigh = (ITypeNeighbor) j.next();
226: int neighPos = neigh.getColor() - 1;
227: Edge currEdge = new Edge(currNode,
228: newNodes[neighPos], neigh
229: .getTransition());
230: }
231:
232: // starting node
233: if (g.getInit().getId() == origNodeId) {
234: result.setInit(currNode);
235: }
236:
237: // accepting node
238: if (isAccepting(g.getNode(origNodeId))) {
239: currNode.setBooleanAttribute("accepting", true);
240: }
241: } else {
242: } // ignore such transitions
243: }
244: }
245:
246: return reachabilityGraph(result);
247:
248: //return result;
249: }
250:
251: private static boolean isAccepting(Node nodeIn) {
252: return (nodeIn.getBooleanAttribute("accepting"));
253: }
254:
255: private static TreeSet getPrevN(Node currNode, boolean[][] prevPO) {
256: List edges = currNode.getOutgoingEdges();
257: LinkedList neighbors = new LinkedList();
258: ITypeNeighbor iNeigh;
259: TreeSet prevN = new TreeSet();
260:
261: for (Iterator i = edges.iterator(); i.hasNext();) {
262: Edge currEdge = (Edge) i.next();
263: iNeigh = new ITypeNeighbor(currEdge.getNext()
264: .getIntAttribute("_prevColor"), currEdge.getGuard());
265: neighbors.add(iNeigh);
266: }
267:
268: // No neighbors present
269: if (neighbors.size() == 0) {
270: return prevN;
271: }
272:
273: // Get the first of the list. Remove it from the list. Compare
274: // this element with the rest of the list. If element subsumes
275: // something in remainder of list remove that thing from list. If
276: // element is subsumed, throw element away, else put element in
277: // set
278: boolean useless;
279:
280: do {
281: useless = false;
282: iNeigh = (ITypeNeighbor) neighbors.removeFirst();
283:
284: for (Iterator i = neighbors.iterator(); i.hasNext();) {
285: ITypeNeighbor nNeigh = (ITypeNeighbor) i.next();
286: ITypeNeighbor dominating = iDominates(iNeigh, nNeigh,
287: prevPO);
288:
289: if (dominating == iNeigh) {
290: i.remove();
291: }
292:
293: if (dominating == nNeigh) {
294: useless = true;
295:
296: break;
297: }
298: }
299:
300: if (!useless) {
301: prevN.add(iNeigh);
302: }
303: } while (neighbors.size() > 0);
304:
305: return prevN;
306: }
307:
308: private static boolean iDominateSet(TreeSet setOne, TreeSet setTwo,
309: boolean[][] prevPO) {
310: TreeSet working = new TreeSet(setTwo);
311:
312: for (Iterator i = working.iterator(); i.hasNext();) {
313: ITypeNeighbor neighTwo = (ITypeNeighbor) i.next();
314:
315: for (Iterator j = setOne.iterator(); j.hasNext();) {
316: ITypeNeighbor neighOne = (ITypeNeighbor) j.next();
317: ITypeNeighbor dominating = iDominates(neighOne,
318: neighTwo, prevPO);
319:
320: if (dominating == neighOne) {
321: i.remove();
322:
323: break;
324: }
325: }
326: }
327:
328: if (working.size() == 0) {
329: return true;
330: }
331:
332: return false;
333: }
334:
335: /** Returns the neighbor that dominates. If none dominates the
336: * other, then returns null
337: */
338: private static ITypeNeighbor iDominates(ITypeNeighbor iNeigh,
339: ITypeNeighbor nNeigh, boolean[][] prevPO) {
340: String iTerm = iNeigh.getTransition();
341: String nTerm = nNeigh.getTransition();
342: int iColor = iNeigh.getColor();
343: int nColor = nNeigh.getColor();
344: String theSubterm = subterm(iTerm, nTerm);
345:
346: if (theSubterm == iTerm) {
347: if (prevPO[nColor - 1][iColor - 1]) {
348: // iNeigh i-dominates nNeigh
349: return iNeigh;
350: } else {
351: return null;
352: }
353: }
354:
355: if (theSubterm == nTerm) {
356: if (prevPO[iColor - 1][nColor - 1]) {
357: // nNeigh i-dominates iNeigh
358: return nNeigh;
359: } else {
360: return null;
361: }
362: }
363:
364: if (theSubterm.equals("true")) {
365: if (prevPO[nColor - 1][iColor - 1]) {
366: // iNeigh i-dominates nNeigh
367: return iNeigh;
368: } else if (prevPO[iColor - 1][nColor - 1]) {
369: // nNeigh i-dominates iNeigh
370: return nNeigh;
371: }
372: }
373:
374: return null;
375: }
376:
377: private static Graph reachabilityGraph(Graph g) {
378: Vector work = new Vector();
379: Vector reachable = new Vector();
380: work.add(g.getInit());
381:
382: while (!work.isEmpty()) {
383: Node currNode = (Node) work.firstElement();
384: reachable.add(currNode);
385:
386: if (currNode != null) {
387: List outgoingEdges = currNode.getOutgoingEdges();
388:
389: for (Iterator i = outgoingEdges.iterator(); i.hasNext();) {
390: Edge currEdge = (Edge) i.next();
391: Node nextNode = (Node) currEdge.getNext();
392:
393: if (!(work.contains(nextNode) || reachable
394: .contains(nextNode))) {
395: work.add(nextNode);
396: }
397: }
398: }
399:
400: if (work.remove(0) != currNode) {
401: System.out.println("ERROR"); // should probably throw exception
402: }
403: }
404:
405: List nodes = g.getNodes();
406:
407: if (nodes != null) {
408: for (Iterator i = nodes.iterator(); i.hasNext();) {
409: Node n = (Node) i.next();
410:
411: if (!reachable.contains(n)) {
412: g.removeNode(n);
413: }
414: }
415: }
416:
417: return g;
418: }
419:
420: private static String subterm(String pred1, String pred2) {
421: if (pred1.equals("-") && pred2.equals("-")) {
422: return "true";
423: }
424:
425: if (pred1.equals("-")) {
426: return pred1;
427: }
428:
429: if (pred2.equals("-")) {
430: return pred2;
431: }
432:
433: if ((pred1.indexOf("true") != -1)
434: && (pred2.indexOf("true") != -1)) {
435: return "true";
436: }
437:
438: if (pred1.indexOf("true") != -1) {
439: return pred1;
440: }
441:
442: if (pred2.indexOf("true") != -1) {
443: return pred2;
444: }
445:
446: // ASSUMPTION: the shortest predicate, i.e. with less litterals,
447: // will most probably be the subterm of the other predicate
448: // (provided terms are simplified)
449: // alpha subterm of tau, i.e. tau implies alpha
450: String alphaStr;
451: String tauStr;
452:
453: if (pred1.length() <= pred2.length()) {
454: alphaStr = pred1;
455: tauStr = pred2;
456: } else {
457: alphaStr = pred2;
458: tauStr = pred1;
459: }
460:
461: StringTokenizer alphaTk = new StringTokenizer(alphaStr, "&");
462: StringTokenizer tauTk = new StringTokenizer(tauStr, "&");
463: LinkedList tauLst = new LinkedList();
464:
465: // Putting the litterals of tau in a list - for easier access
466: while (tauTk.hasMoreTokens()) {
467: String token = tauTk.nextToken();
468: tauLst.add(token);
469: }
470:
471: while (alphaTk.hasMoreTokens()) {
472: String alphaLit = alphaTk.nextToken();
473:
474: if (!tauLst.contains(alphaLit)) {
475: return "false";
476: }
477: }
478:
479: if (pred1.length() == pred2.length()) {
480: return "true";
481: }
482:
483: return alphaStr;
484: }
485: }
|