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:
020: //Written by Dimitra Giannakopoulou, 29 Jan 2001
021: package gov.nasa.ltl.trans;
022:
023: import java.util.*;
024:
025: /**
026: * DOCUMENT ME.
027: */
028: class State implements Comparable {
029: private int representativeId = -1;
030: private LinkedList transitions;
031: private BitSet accepting;
032: private boolean safety_acceptance;
033:
034: public State(BitSet acc) {
035: transitions = new LinkedList();
036: accepting = acc;
037: safety_acceptance = false;
038: }
039:
040: public State(BitSet acc, int equivId) {
041: transitions = new LinkedList();
042: accepting = acc;
043: safety_acceptance = false;
044: representativeId = equivId;
045: }
046:
047: public State() {
048: transitions = new LinkedList();
049: accepting = null;
050: safety_acceptance = false;
051: }
052:
053: public State(int equivId) {
054: transitions = new LinkedList();
055: accepting = null;
056: safety_acceptance = false;
057: representativeId = equivId;
058: }
059:
060: /* public boolean isAccepting()
061: {
062: return accepting;
063: }
064: */
065: public void FSPoutput() {
066: ListIterator iter = transitions.listIterator(0);
067: Transition nextTrans;
068: boolean first_trans = true;
069:
070: while (iter.hasNext()) {
071: nextTrans = (Transition) iter.next();
072:
073: if (first_trans) {
074: System.out.print("(");
075: first_trans = false;
076: } else {
077: System.out.print("|");
078: }
079:
080: nextTrans.FSPoutput();
081: }
082: }
083:
084: public void SMoutput(gov.nasa.ltl.graph.Node[] nodes,
085: gov.nasa.ltl.graph.Node node) {
086: ListIterator iter = transitions.listIterator(0);
087: Transition nextTrans;
088: boolean first_trans = true;
089:
090: while (iter.hasNext()) {
091: nextTrans = (Transition) iter.next();
092: nextTrans.SMoutput(nodes, node);
093: }
094: }
095:
096: public boolean accepts(int i) {
097: return (!(accepting.get(i)));
098:
099: // because in my accepting array 0 corresponds to accepting
100: }
101:
102: // <2do> pcm - CodeGuide Sapphire bug - need to explicitly qualify Transition
103: // or it's mocking its use in Node
104: public void add(Transition trans) {
105: transitions.add(trans);
106: }
107:
108: public int compareTo(Object f) {
109: if (this == f) {
110: return 0;
111: } else {
112: return 1;
113: }
114: }
115:
116: public int get_representativeId() {
117: return representativeId;
118: }
119:
120: public boolean is_safe() {
121: return safety_acceptance;
122: }
123:
124: public void set_representativeId(int id) {
125: representativeId = id;
126: }
127:
128: public void step(Hashtable ProgramState, TreeSet newStates,
129: State[] automaton) {
130: ListIterator iter = transitions.listIterator(0);
131: Transition nextTrans;
132:
133: while (iter.hasNext()) {
134: nextTrans = (Transition) iter.next();
135:
136: if (nextTrans.enabled(ProgramState)) {
137: newStates.add(automaton[nextTrans.goesTo()]);
138: }
139: }
140: }
141:
142: public void update_acc(BitSet acc) {
143: accepting = acc;
144: }
145:
146: public void update_acc(BitSet acc, int equivId) {
147: accepting = acc;
148: representativeId = equivId;
149: }
150:
151: public void update_safety_acc(boolean val) {
152: safety_acceptance = val;
153: }
154: }
|