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.BitSet;
024: import java.util.Iterator;
025: import java.util.List;
026:
027: /**
028: * DOCUMENT ME!
029: */
030: public class SCCReduction {
031: public static void main(String[] args) {
032: if (args.length > 1) {
033: System.out.println("usage:");
034: System.out
035: .println("\tjava gov.nasa.ltl.graph.SCCReduction [<filename>]");
036:
037: return;
038: }
039:
040: Graph g = null;
041:
042: try {
043: if (args.length == 0) {
044: g = Graph.load();
045: } else {
046: g = Graph.load(args[0]);
047: }
048: } catch (IOException e) {
049: System.out.println("Can't load the graph.");
050:
051: return;
052: }
053:
054: g = reduce(g);
055:
056: g.save();
057: }
058:
059: public static Graph reduce(Graph g) {
060: boolean changed;
061: String type = g.getStringAttribute("type");
062: String ac = g.getStringAttribute("ac");
063: boolean acNodes = ac.equals("nodes");
064:
065: for (Iterator i = SCC.scc(g).iterator(); i.hasNext();) {
066: clearExternalEdges((List) i.next(), g);
067: }
068:
069: do {
070: changed = false;
071:
072: List sccs = SCC.scc(g);
073:
074: for (Iterator i = sccs.iterator(); i.hasNext();) {
075: List scc = (List) i.next();
076: boolean accepting = isAccepting(scc, g);
077:
078: if (!accepting && isTerminal(scc)) {
079: changed = true;
080:
081: for (Iterator j = scc.iterator(); j.hasNext();) {
082: ((Node) j.next()).remove();
083: }
084: } else if (isTransient(scc) || !accepting) {
085: changed |= anyAcceptingState(scc, g);
086: clearAccepting(scc, g);
087: }
088: }
089: } while (changed);
090:
091: return g;
092: }
093:
094: private static boolean isAccepting(List scc, Graph g) {
095: String type = g.getStringAttribute("type");
096: String ac = g.getStringAttribute("ac");
097:
098: if (type.equals("ba")) {
099: if (ac.equals("nodes")) {
100: for (Iterator i = scc.iterator(); i.hasNext();) {
101: if (((Node) i.next())
102: .getBooleanAttribute("accepting")) {
103: return true;
104: }
105: }
106:
107: return false;
108: } else if (ac.equals("edges")) {
109: for (Iterator i = scc.iterator(); i.hasNext();) {
110: Node n = (Node) i.next();
111:
112: for (Iterator j = n.getOutgoingEdges().iterator(); j
113: .hasNext();) {
114: Edge e = (Edge) j.next();
115:
116: if (e.getBooleanAttribute("accepting")) {
117: return true;
118: }
119: }
120: }
121:
122: return false;
123: } else {
124: throw new RuntimeException("invalid accepting type: "
125: + ac);
126: }
127: } else if (type.equals("gba")) {
128: int nsets = g.getIntAttribute("nsets");
129: BitSet found = new BitSet(nsets);
130: int nsccs = 0;
131:
132: if (ac.equals("nodes")) {
133: for (Iterator i = scc.iterator(); i.hasNext();) {
134: Node n = (Node) i.next();
135:
136: for (int j = 0; j < nsets; j++) {
137: if (n.getBooleanAttribute("acc" + j)) {
138: if (!found.get(j)) {
139: found.set(j);
140: nsccs++;
141: }
142: }
143: }
144: }
145: } else if (ac.equals("edges")) {
146: for (Iterator i = scc.iterator(); i.hasNext();) {
147: Node n = (Node) i.next();
148:
149: for (Iterator j = n.getOutgoingEdges().iterator(); j
150: .hasNext();) {
151: Edge e = (Edge) j.next();
152:
153: for (int k = 0; k < nsets; k++) {
154: if (e.getBooleanAttribute("acc" + k)) {
155: if (!found.get(k)) {
156: found.set(k);
157: nsccs++;
158: }
159: }
160: }
161: }
162: }
163: } else {
164: throw new RuntimeException("invalid accepting type: "
165: + ac);
166: }
167:
168: return nsccs == nsets;
169: } else {
170: throw new RuntimeException("invalid graph type: " + type);
171: }
172: }
173:
174: private static boolean isTerminal(List scc) {
175: for (Iterator i = scc.iterator(); i.hasNext();) {
176: Node n = (Node) i.next();
177:
178: for (Iterator j = n.getOutgoingEdges().iterator(); j
179: .hasNext();) {
180: if (!scc.contains(((Edge) j.next()).getNext())) {
181: return false;
182: }
183: }
184: }
185:
186: return true;
187: }
188:
189: private static boolean isTransient(List scc) {
190: if (scc.size() != 1) {
191: return false;
192: }
193:
194: Node n = (Node) scc.get(0);
195:
196: for (Iterator i = n.getOutgoingEdges().iterator(); i.hasNext();) {
197: if (((Edge) i.next()).getNext() == n) {
198: return false;
199: }
200: }
201:
202: return true;
203: }
204:
205: private static boolean anyAcceptingState(List scc, Graph g) {
206: String type = g.getStringAttribute("type");
207: String ac = g.getStringAttribute("ac");
208:
209: if (type.equals("ba")) {
210: if (ac.equals("nodes")) {
211: for (Iterator i = scc.iterator(); i.hasNext();) {
212: Node n = (Node) i.next();
213:
214: if (n.getBooleanAttribute("accepting")) {
215: return true;
216: }
217: }
218: } else if (ac.equals("edges")) {
219: for (Iterator i = scc.iterator(); i.hasNext();) {
220: Node n = (Node) i.next();
221:
222: for (Iterator j = n.getOutgoingEdges().iterator(); j
223: .hasNext();) {
224: Edge e = (Edge) j.next();
225:
226: if (e.getBooleanAttribute("accepting")) {
227: return true;
228: }
229: }
230: }
231: } else {
232: throw new RuntimeException("invalid accepting type: "
233: + ac);
234: }
235: } else if (type.equals("gba")) {
236: int nsets = g.getIntAttribute("nsets");
237:
238: if (ac.equals("nodes")) {
239: for (Iterator i = scc.iterator(); i.hasNext();) {
240: Node n = (Node) i.next();
241:
242: for (int j = 0; j < nsets; j++) {
243: if (n.getBooleanAttribute("acc" + j)) {
244: return true;
245: }
246: }
247: }
248: } else if (ac.equals("edges")) {
249: for (Iterator i = scc.iterator(); i.hasNext();) {
250: Node n = (Node) i.next();
251:
252: for (Iterator j = n.getOutgoingEdges().iterator(); j
253: .hasNext();) {
254: Edge e = (Edge) j.next();
255:
256: for (int k = 0; k < nsets; k++) {
257: if (e.getBooleanAttribute("acc" + j)) {
258: return true;
259: }
260: }
261: }
262: }
263: } else {
264: throw new RuntimeException("invalid accepting type: "
265: + ac);
266: }
267: } else {
268: throw new RuntimeException("invalid graph type: " + type);
269: }
270:
271: return false;
272: }
273:
274: private static void clearAccepting(List scc, Graph g) {
275: String type = g.getStringAttribute("type");
276: String ac = g.getStringAttribute("ac");
277:
278: if (type.equals("ba")) {
279: if (ac.equals("nodes")) {
280: for (Iterator i = scc.iterator(); i.hasNext();) {
281: Node n = (Node) i.next();
282:
283: n.setBooleanAttribute("accepting", false);
284: }
285: } else if (ac.equals("edges")) {
286: for (Iterator i = scc.iterator(); i.hasNext();) {
287: Node n = (Node) i.next();
288:
289: for (Iterator j = n.getOutgoingEdges().iterator(); j
290: .hasNext();) {
291: Edge e = (Edge) j.next();
292:
293: e.setBooleanAttribute("accepting", false);
294: }
295: }
296: } else {
297: throw new RuntimeException("invalid accepting type: "
298: + ac);
299: }
300: } else if (type.equals("gba")) {
301: int nsets = g.getIntAttribute("nsets");
302:
303: if (ac.equals("nodes")) {
304: for (Iterator i = scc.iterator(); i.hasNext();) {
305: Node n = (Node) i.next();
306:
307: for (int j = 0; j < nsets; j++) {
308: n.setBooleanAttribute("acc" + j, false);
309: }
310: }
311: } else if (ac.equals("edges")) {
312: for (Iterator i = scc.iterator(); i.hasNext();) {
313: Node n = (Node) i.next();
314:
315: for (Iterator j = n.getOutgoingEdges().iterator(); j
316: .hasNext();) {
317: Edge e = (Edge) j.next();
318:
319: for (int k = 0; k < nsets; k++) {
320: e.setBooleanAttribute("acc" + k, false);
321: }
322: }
323: }
324: } else {
325: throw new RuntimeException("invalid accepting type: "
326: + ac);
327: }
328: } else {
329: throw new RuntimeException("invalid graph type: " + type);
330: }
331: }
332:
333: private static void clearExternalEdges(List scc, Graph g) {
334: String type = g.getStringAttribute("type");
335: String ac = g.getStringAttribute("ac");
336:
337: if (type.equals("ba")) {
338: if (ac.equals("nodes")) {
339: } else if (ac.equals("edges")) {
340: for (Iterator i = scc.iterator(); i.hasNext();) {
341: Node n = (Node) i.next();
342:
343: for (Iterator j = n.getOutgoingEdges().iterator(); j
344: .hasNext();) {
345: Edge e = (Edge) j.next();
346:
347: if (!scc.contains(e.getNext())) {
348: e.setBooleanAttribute("accepting", false);
349: }
350: }
351: }
352: } else {
353: throw new RuntimeException("invalid accepting type: "
354: + ac);
355: }
356: } else if (type.equals("gba")) {
357: int nsets = g.getIntAttribute("nsets");
358:
359: if (ac.equals("nodes")) {
360: } else if (ac.equals("edges")) {
361: for (Iterator i = scc.iterator(); i.hasNext();) {
362: Node n = (Node) i.next();
363:
364: for (Iterator j = n.getOutgoingEdges().iterator(); j
365: .hasNext();) {
366: Edge e = (Edge) j.next();
367:
368: if (!scc.contains(e.getNext())) {
369: for (int k = 0; k < nsets; k++) {
370: e.setBooleanAttribute("acc" + k, false);
371: }
372: }
373: }
374: }
375: } else {
376: throw new RuntimeException("invalid accepting type: "
377: + ac);
378: }
379: } else {
380: throw new RuntimeException("invalid graph type: " + type);
381: }
382: }
383: }
|