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.jpf;
020:
021: import gov.nasa.jpf.util.Printable;
022:
023: import java.io.PrintWriter;
024:
025: import java.util.LinkedList;
026:
027: /**
028: * Path represents the data structure in which a execution trace is recorded.
029: *
030: * It usually gets created by a VirtualMachine, can be stored in a file
031: * via the JPF '-save-path' option, re-executed with '-execute-path', or
032: * explicitly loaded via 'JPF.loadPath(fileName)'
033: *
034: * A path instance is specific to a certain 'application', and consists of a
035: * list of 'Transition' objects
036: */
037: public class Path implements Printable {
038: String application;
039: private LinkedList list;
040:
041: public Path(String app) {
042: application = app;
043: list = new LinkedList();
044: }
045:
046: private Path(String app, LinkedList l) {
047: application = app;
048: list = l;
049: }
050:
051: public String getApplication() {
052: return application;
053: }
054:
055: public Transition getLast() {
056: if (list.size() > 0) {
057: return (Transition) list.getLast();
058: } else {
059: return null;
060: }
061: }
062:
063: public void add(Transition t) {
064: list.add(t);
065: }
066:
067: public Object clone() {
068: // <2do> clone path elements, too
069: return new Path(application, (LinkedList) list.clone());
070: }
071:
072: public Transition get(int pos) {
073: return (Transition) list.get(pos);
074: }
075:
076: public int length() {
077: return list.size();
078: }
079:
080: public boolean hasOutput() {
081: int len = list.size();
082: for (int i = 0; i < len; i++) {
083: Transition t = (Transition) list.get(i);
084: if (t.getOutput() != null) {
085: return true;
086: }
087: }
088:
089: return false;
090: }
091:
092: public void printOutputOn(PrintWriter pw) {
093: int i;
094: int length = list.size();
095: Transition t;
096: String s;
097:
098: for (i = 0; i < length; i++) {
099: t = (Transition) list.get(i);
100: s = t.getOutput();
101: if (s != null) {
102: pw.print(s);
103: }
104: }
105: }
106:
107: public void printOn(PrintWriter pw) {
108: int length = list.size();
109: Object entry;
110:
111: for (int index = 0; index < length; index++) {
112: pw.print("Transition #");
113: pw.print(index);
114:
115: if ((entry = list.get(index)) != null) {
116: pw.print(' ');
117:
118: if (entry instanceof Printable) {
119: ((Printable) entry).printOn(pw);
120: } else {
121: pw.print(entry);
122: pw.flush();
123: }
124: }
125: }
126: }
127:
128: public void removeLast() {
129: list.removeLast();
130: }
131: }
|