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, 19 Jan 2001
021: package gov.nasa.ltl.trans;
022:
023: import java.util.*;
024:
025: /**
026: * DOCUMENT ME!
027: */
028: class Node implements Comparable {
029: public static int accepting_conds = 0;
030: private static boolean init_collapsed = false;
031: private int nodeId;
032: private TreeSet incoming;
033: private TreeSet toBeDone;
034: private TreeSet old;
035: private TreeSet next;
036: private BitSet accepting;
037: private BitSet right_of_untils;
038: private Node OtherTransitionSource;
039: private int equivalenceId;
040:
041: public Node() {
042: nodeId = Pool.assign();
043: incoming = new TreeSet();
044: toBeDone = new TreeSet();
045: old = new TreeSet();
046: next = new TreeSet();
047: OtherTransitionSource = null;
048: accepting = new BitSet(accepting_conds);
049: right_of_untils = new BitSet(accepting_conds);
050: }
051:
052: public Node(TreeSet in, TreeSet newForm, TreeSet done, TreeSet nx,
053: BitSet acc, BitSet rous) {
054: nodeId = Pool.assign();
055: incoming = new TreeSet(in);
056: toBeDone = new TreeSet(newForm);
057: old = new TreeSet(done);
058: next = new TreeSet(nx);
059: OtherTransitionSource = null;
060: accepting = new BitSet(accepting_conds);
061: accepting.or(acc);
062: right_of_untils = new BitSet(accepting_conds);
063: right_of_untils.or(rous);
064: }
065:
066: public static int getAcceptingConds() {
067: return accepting_conds;
068: }
069:
070: public static Node createInitial(Formula form) {
071: accepting_conds = form.initialize(); // first mark right forms of untils;
072:
073: // System.out.println("Accepting conditions: " + accepting_conds);
074: Node init = new Node();
075: init.nodeId = 0;
076:
077: if (form.getContent() != 't') {
078: init.decompose_ands_for_next(form);
079: }
080:
081: return init;
082: }
083:
084: public static void reset_static() {
085: accepting_conds = 0;
086: init_collapsed = false;
087: }
088:
089: public TreeSet getField_next() {
090: return next;
091: }
092:
093: public TreeSet getField_old() {
094: return old;
095: }
096:
097: public int getId() {
098: return nodeId;
099: }
100:
101: public boolean isInitial() {
102: return nodeId == 0;
103: }
104:
105: public int getNodeId() {
106: return nodeId;
107: }
108:
109: public void RTstructure(State[] RTautomaton) {
110: boolean safety = false;
111:
112: if (RTautomaton[nodeId] == null) {
113: RTautomaton[nodeId] = new State(accepting, equivalenceId);
114: } else {
115: RTautomaton[nodeId].update_acc(accepting, equivalenceId);
116: }
117:
118: if (is_safety_acc_node()) {
119: RTautomaton[nodeId].update_safety_acc(true);
120: safety = true;
121: }
122:
123: Node Alternative = this ;
124:
125: while (Alternative != null) {
126: Iterator iterIncom = Alternative.incoming.iterator();
127: Node nextNode;
128:
129: while (iterIncom.hasNext()) {
130: nextNode = (Node) iterIncom.next();
131:
132: int stateId = nextNode.getId();
133:
134: if (RTautomaton[stateId] == null) {
135: RTautomaton[stateId] = new State();
136: }
137:
138: RTautomaton[stateId].add(new Transition(
139: Alternative.old, equivalenceId, accepting,
140: safety));
141: }
142:
143: Alternative = Alternative.OtherTransitionSource;
144: }
145: }
146:
147: public int compareTo(Object f) {
148: if (this == f) {
149: return 0;
150: } else {
151: return 1;
152: }
153: }
154:
155: public boolean compare_accepting(Node nd) {
156: //if (nodeId == 0)
157: // System.out.println("Has it been collapsed yet? : " + init_collapsed);
158: if ((nodeId == 0) && !init_collapsed) {
159: // System.out.println("Potentially collapse " + nodeId + " with " + nd.nodeId);
160: return true;
161: }
162:
163: return (accepting.equals(nd.accepting)); // compare their BitSets
164: }
165:
166: /*
167: public void print()
168: {
169: System.out.println("\n\nPrinting node " + nodeId);
170: Iterator iterNext = next.iterator();
171: Formula nextForm = null;
172:
173: // all formulas present must be of type V or W, otherwise false
174: while (iterNext.hasNext())
175: {
176: nextForm = (Formula) iterNext.next();
177: System.out.println("Formula: " + nextForm.toString());
178: }
179: }
180: */
181: public void debug() {
182: Iterator iterOld = old.iterator();
183: Formula nextForm = null;
184:
185: // System.out.println("debugging now");
186: while (iterOld.hasNext()) {
187: nextForm = (Formula) iterOld.next();
188:
189: // System.out.println("Content is " + nextForm.getContent());
190: }
191: }
192:
193: public void decompose_ands_for_next(Formula form) {
194: if (form.getContent() == 'A') {
195: decompose_ands_for_next(form.getSub1());
196: decompose_ands_for_next(form.getSub2());
197: } else if (is_redundant(next, null, form) == false) {
198: next.add(form);
199: }
200: }
201:
202: public Automaton expand(Automaton states) {
203: // System.out.println("expand entered"); // debugging
204: Node tempNode;
205:
206: if (toBeDone.isEmpty()) {
207: if (nodeId != 0) {
208: update_accepting();
209: }
210:
211: // System.out.println("New is empty!");
212: tempNode = states.alreadyThere(this );
213:
214: if (tempNode != null) {
215: // System.out.println("Node " + nodeId + " collapsed with " + tempNode.nodeId);
216: tempNode.modify(this );
217:
218: return states;
219: } else {
220: Node NewN = new Node();
221: NewN.incoming.add(this );
222: NewN.toBeDone.addAll(next);
223:
224: states.add(this );
225:
226: return (NewN.expand(states));
227: }
228: } else // toBeDone is not empty
229: {
230: Formula temp_form;
231: Formula ita = (Formula) toBeDone.first();
232: toBeDone.remove(ita);
233:
234: //System.out.println("\n\nExpanding " + ita + " for node " + nodeId);
235: if (testForContradictions(ita)) {
236: //System.out.println("Finished expand - contradiction");
237: return states;
238: }
239:
240: // no contradiction
241: // look in tech report why we do this even when ita is redundant
242: if (ita.is_right_of_until(accepting_conds)) {
243: right_of_untils.or(ita.get_rightOfWhichUntils());
244: }
245:
246: TreeSet set_checked_against = new TreeSet();
247: set_checked_against.addAll(old);
248: set_checked_against.addAll(toBeDone);
249:
250: if (is_redundant(set_checked_against, next, ita)) {
251: return expand(states);
252: }
253:
254: // not redundant either
255: // look in tech report why this only when not redundant
256: if (ita.getContent() == 'U') { // this is an until formula
257: accepting.set(ita.get_untils_index());
258:
259: // System.out.println("Just set an eventuality requirement");
260: }
261:
262: if (!ita.is_literal()) {
263: switch (ita.getContent()) {
264: case 'U':
265: case 'W':
266: case 'V':
267: case 'O':
268:
269: Node node2 = split(ita);
270:
271: return node2.expand(this .expand(states));
272:
273: case 'X':
274: decompose_ands_for_next(ita.getSub1());
275:
276: return expand(states);
277:
278: case 'A':
279: temp_form = ita.getSub1();
280:
281: if (!old.contains(temp_form)) {
282: toBeDone.add(temp_form);
283: }
284:
285: temp_form = ita.getSub2();
286:
287: if (!old.contains(temp_form)) {
288: toBeDone.add(temp_form);
289: }
290:
291: return expand(states);
292:
293: default:
294: System.out
295: .println("default case of switch entered");
296:
297: return null;
298: }
299: } else // ita represents a literal
300: {
301: // System.out.println("Now working on literal " + ita.getContent());
302: // must do a test for contradictions first
303: if (ita.getContent() != 't') {
304: old.add(ita);
305: }
306:
307: // System.out.println("added to " + nodeId + " formula " + ita);
308: return (expand(states));
309: }
310: }
311: }
312:
313: public int get_equivalenceId() {
314: return equivalenceId;
315: }
316:
317: public void set_equivalenceId(int value) {
318: equivalenceId = value;
319: }
320:
321: public void update_accepting() {
322: accepting.andNot(right_of_untils);
323:
324: // just do now the bitwise or so that accepting gets updated
325: }
326:
327: private static boolean is_redundant(TreeSet main_set,
328: TreeSet next_set, Formula ita) {
329: if ((ita.is_special_case_of_V(main_set)) || // my addition - correct???
330: ((ita.is_synt_implied(main_set, next_set)) && (!(ita
331: .getContent() == 'U') || (ita.getSub2()
332: .is_synt_implied(main_set, next_set))))) {
333: //System.out.println("Looks like formula was redundant");
334: return true;
335: } else {
336: return false;
337: }
338: }
339:
340: private boolean is_safety_acc_node() {
341: if (next.isEmpty()) {
342: return true;
343: }
344:
345: Iterator iterNext = next.iterator();
346: Formula nextForm = null;
347:
348: // all formulas present must be of type V or W, otherwise false
349: while (iterNext.hasNext()) {
350: nextForm = (Formula) iterNext.next();
351:
352: if ((nextForm.getContent() != 'V')
353: && (nextForm.getContent() != 'W')) {
354: return false;
355: }
356: }
357:
358: return true;
359: }
360:
361: private void modify(Node current) {
362: boolean match = false;
363: Node Tail = this ;
364: Node Alternative = this ;
365:
366: if ((this .nodeId == 0) && !init_collapsed) {
367: accepting = current.accepting;
368: init_collapsed = true;
369: }
370:
371: while (Alternative != null) {
372: if (Alternative.old.equals(current.old)) {
373: Alternative.incoming.addAll(current.incoming);
374: match = true;
375: }
376:
377: Tail = Alternative;
378: Alternative = Alternative.OtherTransitionSource;
379: }
380:
381: if (!match) {
382: Tail.OtherTransitionSource = current;
383: }
384: }
385:
386: private Node split(Formula form) {
387: //System.out.println("Split is entered");
388: Formula temp_form;
389:
390: // first create Node 2
391: Node Node2 = new Node(this .incoming, this .toBeDone, this .old,
392: this .next, this .accepting, this .right_of_untils);
393:
394: temp_form = form.getSub2();
395:
396: if (!old.contains(temp_form)) //New2(n) not in old
397:
398: {
399: Node2.toBeDone.add(temp_form);
400: }
401:
402: if (form.getContent() == 'V') // both subformulas are added to New2
403: {
404: temp_form = form.getSub1();
405:
406: if (!old.contains(temp_form)) // subformula not in old
407:
408: {
409: Node2.toBeDone.add(temp_form);
410: }
411: }
412:
413: // then substitute current Node with Node 1
414: temp_form = form.getSub1();
415:
416: if (!old.contains(temp_form)) //New1(n) not in old
417:
418: {
419: toBeDone.add(temp_form);
420: }
421:
422: temp_form = form.getNext();
423:
424: if (temp_form != null) {
425: decompose_ands_for_next(temp_form);
426: }
427:
428: /* following lines are probably unecessary because we never split literals!*/
429: if (form.is_literal())/* because we only store literals... */
430: {
431: old.add(form);
432: System.out.println("added " + form); // never supposed to see that
433: Node2.old.add(form);
434: }
435:
436: //System.out.println("Node split into itself and node : " + Node2.nodeId);
437: //print();
438: //Node2.print();
439: return Node2;
440: }
441:
442: private boolean testForContradictions(Formula ita) {
443: Formula Not_ita = ita.negate();
444:
445: if (Not_ita.is_synt_implied(old, next)) {
446: return true;
447: } else {
448: return false;
449: }
450: }
451: }
|