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.trans;
020:
021: import gov.nasa.ltl.graph.*;
022:
023: import java.util.*;
024:
025: /**
026: * DOCUMENT ME!
027: */
028: class Transition {
029: private TreeSet propositions;
030: private int pointsTo;
031: private BitSet accepting;
032: private boolean safe_accepting;
033:
034: public Transition(TreeSet prop, int nd_id, BitSet acc,
035: boolean safety) {
036: propositions = prop;
037: pointsTo = nd_id;
038: accepting = new BitSet(Node.getAcceptingConds());
039: accepting.or(acc);
040: safe_accepting = safety;
041: }
042:
043: public void FSPoutput() {
044: if (propositions.isEmpty()) {
045: System.out.print("TRUE{");
046: } else {
047: // first print the propositions involved
048: Iterator it = propositions.iterator();
049: Formula nextForm = null;
050: StringBuffer act = new StringBuffer();
051: char cont; // stores content of formula
052: boolean need_AND = false; // connect with AND multiple propositions
053:
054: while (it.hasNext()) {
055: nextForm = (Formula) it.next();
056: cont = nextForm.getContent();
057:
058: if (need_AND) {
059: act.append("_AND_");
060: }
061:
062: need_AND = true;
063:
064: switch (cont) {
065: case 'N':
066: act.append('N');
067: act.append(nextForm.getSub1().getName());
068:
069: break;
070:
071: case 't':
072: act.append("TRUE");
073:
074: break;
075:
076: default:
077: act.append(nextForm.getName());
078:
079: break;
080: }
081: }
082:
083: System.out.print(act + "{");
084: }
085:
086: if (Node.accepting_conds == 0) {
087: if (safe_accepting == true) {
088: System.out.print("0");
089: }
090: } else {
091: for (int i = 0; i < Node.accepting_conds; i++) {
092: if (!accepting.get(i)) {
093: System.out.print(i);
094: }
095: }
096: }
097:
098: // and then the rest - easy
099: System.out.print("} -> S" + pointsTo + " ");
100: }
101:
102: public void SMoutput(gov.nasa.ltl.graph.Node[] nodes,
103: gov.nasa.ltl.graph.Node node) {
104: String guard = "-";
105: String action = "-";
106:
107: if (!propositions.isEmpty()) {
108: Iterator it = propositions.iterator();
109: Formula nextForm = null;
110: StringBuffer sb = new StringBuffer();
111: char cont; // stores content of formula
112: boolean need_AND = false; // connect with AND multiple propositions
113:
114: while (it.hasNext()) {
115: nextForm = (Formula) it.next();
116: cont = nextForm.getContent();
117:
118: if (need_AND) {
119: sb.append("&");
120: }
121:
122: need_AND = true;
123:
124: switch (cont) {
125: case 'N':
126: sb.append('!');
127: sb.append(nextForm.getSub1().getName());
128:
129: break;
130:
131: case 't':
132: sb.append("true");
133:
134: break;
135:
136: default:
137: sb.append(nextForm.getName());
138:
139: break;
140: }
141: }
142:
143: guard = sb.toString();
144: }
145:
146: Edge e = new Edge(node, nodes[pointsTo], guard, action);
147:
148: if (Node.accepting_conds == 0) {
149: // Dimitra - Jan 10 2003
150: // Believe there is a bug with the way we decided whether node was safety accepting
151: // with example !<>(Xa \/ <>c)
152: // System.out.println("Entered the safety part of accepting conditions");
153: // if (safe_accepting == true) {
154: // System.out.println("But did I actually set it correctly?");
155: e.setBooleanAttribute("acc0", true);
156:
157: // }
158: } else {
159: for (int i = 0; i < Node.accepting_conds; i++) {
160: if (!accepting.get(i)) {
161: e.setBooleanAttribute("acc" + i, true);
162:
163: // System.out.println("Transition belongs to set " + i);
164: }
165: }
166: }
167: }
168:
169: public boolean enabled(Hashtable ProgramState) {
170: Iterator mustHold = propositions.iterator();
171: Formula form = null;
172: char c;
173: Boolean value;
174:
175: while (mustHold.hasNext()) {
176: form = (Formula) mustHold.next();
177:
178: switch (c = form.getContent()) {
179: case 'N':
180: value = (Boolean) ProgramState.get(form.getSub1()
181: .getName());
182:
183: if (value == null) {
184: // System.out.println("Proposition not defined in program state");
185: return false;
186: } else if (value.booleanValue()) {
187: return false;
188: }
189:
190: break;
191:
192: case 't':
193: break;
194:
195: case 'p':
196: value = (Boolean) ProgramState.get(form.getName());
197:
198: if (value == null) {
199: // System.out.println("Proposition not defined in program state");
200: return false;
201: } else if (!value.booleanValue()) {
202: return false;
203: }
204:
205: break;
206: }
207: }
208:
209: return true;
210: }
211:
212: public int goesTo() {
213: return pointsTo;
214: }
215: }
|