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.BufferedReader;
022: import java.io.FileOutputStream;
023: import java.io.FileReader;
024: import java.io.IOException;
025: import java.io.InputStreamReader;
026: import java.io.PrintStream;
027: import java.util.Iterator;
028: import java.util.LinkedList;
029: import java.util.List;
030:
031: /**
032: * DOCUMENT ME!
033: */
034: public class Graph {
035: public static final int SM_FORMAT = 0;
036:
037: public static final int FSP_FORMAT = 1;
038:
039: public static final int XML_FORMAT = 2;
040:
041: public static final int SPIN_FORMAT = 3;
042:
043: private List nodes;
044:
045: private Node init;
046:
047: private Attributes attributes;
048:
049: public Graph(Attributes a) {
050: init(a);
051: }
052:
053: public Graph() {
054: init(null);
055: }
056:
057: public synchronized void setAttributes(Attributes a) {
058: attributes = new Attributes(a);
059: }
060:
061: public synchronized void setBooleanAttribute(String name,
062: boolean value) {
063: attributes.setBoolean(name, value);
064: }
065:
066: public boolean getBooleanAttribute(String name) {
067: return attributes.getBoolean(name);
068: }
069:
070: public int getEdgeCount() {
071: int count = 0;
072:
073: for (Iterator i = new LinkedList(nodes).iterator(); i.hasNext();) {
074: count += ((Node) i.next()).getOutgoingEdgeCount();
075: }
076:
077: return count;
078: }
079:
080: public synchronized void setInit(Node n) {
081: if (nodes.contains(n)) {
082: init = n;
083: number();
084: }
085: }
086:
087: public Node getInit() {
088: return init;
089: }
090:
091: public synchronized void setIntAttribute(String name, int value) {
092: attributes.setInt(name, value);
093: }
094:
095: public int getIntAttribute(String name) {
096: return attributes.getInt(name);
097: }
098:
099: public Node getNode(int id) {
100: for (Iterator i = nodes.iterator(); i.hasNext();) {
101: Node n = (Node) i.next();
102:
103: if (n.getId() == id) {
104: return n;
105: }
106: }
107:
108: return null;
109: }
110:
111: public int getNodeCount() {
112: return nodes.size();
113: }
114:
115: public List getNodes() {
116: return new LinkedList(nodes);
117: }
118:
119: public synchronized void setStringAttribute(String name,
120: String value) {
121: attributes.setString(name, value);
122: }
123:
124: public String getStringAttribute(String name) {
125: return attributes.getString(name);
126: }
127:
128: public static Graph load() throws IOException {
129: return load(new BufferedReader(new InputStreamReader(System.in)));
130: }
131:
132: public static Graph load(String fname) throws IOException {
133: return load(new BufferedReader(new FileReader(fname)));
134: }
135:
136: public synchronized void dfs(Visitor v) {
137: if (init == null) {
138: return;
139: }
140:
141: forAllNodes(new EmptyVisitor() {
142: public void visitNode(Node n) {
143: n.setBooleanAttribute("_reached", false);
144: }
145: });
146:
147: dfs(init, v);
148:
149: forAllNodes(new EmptyVisitor() {
150: public void visitNode(Node n) {
151: n.setBooleanAttribute("_reached", false);
152: }
153: });
154: }
155:
156: public synchronized void forAll(Visitor v) {
157: for (Iterator i = new LinkedList(nodes).iterator(); i.hasNext();) {
158: Node n = (Node) i.next();
159:
160: v.visitNode(n);
161:
162: n.forAllEdges(v);
163: }
164: }
165:
166: public synchronized void forAllEdges(Visitor v) {
167: for (Iterator i = new LinkedList(nodes).iterator(); i.hasNext();) {
168: Node n = (Node) i.next();
169:
170: n.forAllEdges(v);
171: }
172: }
173:
174: public synchronized void forAllNodes(Visitor v) {
175: for (Iterator i = new LinkedList(nodes).iterator(); i.hasNext();) {
176: Node n = (Node) i.next();
177: v.visitNode(n);
178: }
179: }
180:
181: public synchronized void save(int format) {
182: save(System.out, format);
183: }
184:
185: public synchronized void save() {
186: save(System.out, SM_FORMAT);
187: }
188:
189: public synchronized void save(String fname, int format)
190: throws IOException {
191: save(new PrintStream(new FileOutputStream(fname)), format);
192: }
193:
194: public synchronized void save(String fname) throws IOException {
195: save(new PrintStream(new FileOutputStream(fname)), SM_FORMAT);
196: }
197:
198: synchronized void addNode(Node n) {
199: nodes.add(n);
200:
201: if (init == null) {
202: init = n;
203: }
204:
205: number();
206: }
207:
208: synchronized void removeNode(Node n) {
209: nodes.remove(n);
210:
211: if (init == n) {
212: if (nodes.size() != 0) {
213: init = (Node) nodes.get(0);
214: } else {
215: init = null;
216: }
217: }
218:
219: number();
220: }
221:
222: private void init(Attributes a) {
223: if (a == null) {
224: attributes = new Attributes();
225: } else {
226: attributes = a;
227: }
228:
229: nodes = new LinkedList();
230: init = null;
231: }
232:
233: private static Graph load(BufferedReader in) throws IOException {
234: int ns = readInt(in);
235: Node[] nodes = new Node[ns];
236:
237: Graph g = new Graph(readAttributes(in));
238:
239: for (int i = 0; i < ns; i++) {
240: int nt = readInt(in);
241:
242: if (nodes[i] == null) {
243: nodes[i] = new Node(g, readAttributes(in));
244: } else {
245: nodes[i].setAttributes(readAttributes(in));
246: }
247:
248: for (int j = 0; j < nt; j++) {
249: int nxt = readInt(in);
250: String gu = readString(in);
251: String ac = readString(in);
252:
253: if (nodes[nxt] == null) {
254: nodes[nxt] = new Node(g);
255: }
256:
257: new Edge(nodes[i], nodes[nxt], gu, ac,
258: readAttributes(in));
259: }
260: }
261:
262: g.number();
263:
264: return g;
265: }
266:
267: private synchronized void number() {
268: int cnt;
269:
270: if (init != null) {
271: init.setId(0);
272: cnt = 1;
273: } else {
274: cnt = 0;
275: }
276:
277: for (Iterator i = nodes.iterator(); i.hasNext();) {
278: Node n = (Node) i.next();
279:
280: if (n != init) {
281: n.setId(cnt++);
282: }
283: }
284: }
285:
286: private static Attributes readAttributes(BufferedReader in)
287: throws IOException {
288: return new Attributes(readLine(in));
289: }
290:
291: private static int readInt(BufferedReader in) throws IOException {
292: return Integer.parseInt(readLine(in));
293: }
294:
295: private static String readLine(BufferedReader in)
296: throws IOException {
297: String line;
298:
299: do {
300: line = in.readLine();
301:
302: int idx = line.indexOf('#');
303:
304: if (idx != -1) {
305: line = line.substring(0, idx);
306: }
307:
308: line = line.trim();
309: } while (line.length() == 0);
310:
311: return line;
312: }
313:
314: private static String readString(BufferedReader in)
315: throws IOException {
316: return readLine(in);
317: }
318:
319: private synchronized void dfs(Node n, Visitor v) {
320: final Visitor visitor = v;
321:
322: if (n.getBooleanAttribute("_reached")) {
323: return;
324: }
325:
326: n.setBooleanAttribute("_reached", true);
327:
328: v.visitNode(n);
329:
330: n.forAllEdges(new EmptyVisitor() {
331: public void visitEdge(Edge e) {
332: dfs(e.getNext(), visitor);
333: }
334: });
335: }
336:
337: // Modified by robbyjo - Jul 15, 2002
338: private synchronized void save(PrintStream out, int format) {
339: switch (format) {
340: case SM_FORMAT:
341: save_sm(out);
342:
343: break;
344:
345: case FSP_FORMAT:
346: save_fsp(out);
347:
348: break;
349:
350: case XML_FORMAT:
351: save_xml(out);
352:
353: break;
354:
355: case SPIN_FORMAT:
356: save_spin(out);
357:
358: break;
359:
360: default:
361: throw new RuntimeException("Unknown format!");
362: }
363: }
364:
365: // Modified by ckong - Sept 7, 2001
366: private synchronized void save_fsp(PrintStream out) {
367: boolean empty = false;
368:
369: if (init != null) {
370: out.print("RES = S" + init.getId());
371: } else {
372: out.print("Empty");
373: empty = true;
374: }
375:
376: for (Iterator i = nodes.iterator(); i.hasNext();) {
377: //System.out.println(",");
378: out.println(",");
379:
380: Node n = (Node) i.next();
381: n.save(out, FSP_FORMAT);
382: }
383:
384: //System.out.println(".");
385: out.println(".");
386:
387: int nsets = getIntAttribute("nsets");
388:
389: if ((nsets == 0) && !empty) {
390: boolean first = true;
391:
392: //System.out.print("AS = { ");
393: out.print("AS = { ");
394:
395: for (Iterator i = nodes.iterator(); i.hasNext();) {
396: Node n = (Node) i.next();
397:
398: if (n.getBooleanAttribute("accepting")) {
399: if (!first) {
400: //System.out.print(", ");
401: out.print(", ");
402: } else {
403: first = false;
404: }
405:
406: //System.out.print("S" + n.getId());
407: out.print("S" + n.getId());
408: }
409: }
410:
411: //System.out.println(" }");
412: out.println(" }");
413: } else if (!empty) { // nsets != 0
414:
415: for (int k = 0; k < nsets; k++) {
416: boolean first = true;
417:
418: //System.out.print("AS"+k+" = { ");
419: out.print("AS" + k + " = { ");
420:
421: for (Iterator i = nodes.iterator(); i.hasNext();) {
422: Node n = (Node) i.next();
423:
424: if (n.getBooleanAttribute("acc" + k)) {
425: if (!first) {
426: //System.out.print(", ");
427: out.print(", ");
428: } else {
429: first = false;
430: }
431:
432: //System.out.print("S" + n.getId());
433: out.print("S" + n.getId());
434: }
435: }
436:
437: //System.out.println(" }");
438: out.println(" }");
439: }
440: }
441:
442: if (out != System.out) {
443: out.close();
444: }
445: }
446:
447: private synchronized void save_sm(PrintStream out) {
448: out.println(nodes.size());
449: out.println(attributes);
450:
451: if (init != null) {
452: init.save(out, SM_FORMAT);
453: }
454:
455: for (Iterator i = nodes.iterator(); i.hasNext();) {
456: Node n = (Node) i.next();
457:
458: if (n != init) {
459: n.save(out, SM_FORMAT);
460: }
461: }
462: }
463:
464: // robbyjo's contribution
465: private synchronized void save_spin(PrintStream out) {
466: String ln = System.getProperty("line.separator");
467: if (init != null) {
468: out.println("never {");
469: } else {
470: out.println("Empty");
471: return;
472: }
473:
474: init.save(out, SPIN_FORMAT);
475: for (Iterator i = nodes.iterator(); i.hasNext();) {
476: Node n = (Node) i.next();
477:
478: if (init == n) {
479: continue;
480: }
481:
482: n.save(out, SPIN_FORMAT);
483: out.println();
484: }
485:
486: out.println("}");
487: }
488:
489: private synchronized void save_xml(PrintStream out) {
490: out.println("<?xml version=\"1.0\"?>");
491: out.println("<graph nodes=\"" + nodes.size() + "\">");
492: attributes.save(out, XML_FORMAT);
493:
494: for (Iterator i = nodes.iterator(); i.hasNext();) {
495: Node n = (Node) i.next();
496:
497: if (n != init) {
498: n.save(out, XML_FORMAT);
499: } else {
500: n.setBooleanAttribute("init", true);
501: n.save(out, XML_FORMAT);
502: n.setBooleanAttribute("init", false);
503: }
504: }
505:
506: out.println("</graph>");
507: }
508: }
|