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 gov.nasa.ltl.graph.*;
024:
025: /**
026: * DOCUMENT ME!
027: */
028: class LinkNode {
029: private Node node;
030: private LinkNode next;
031:
032: public LinkNode(Node nd, LinkNode nxt) {
033: node = nd;
034: next = nxt;
035: }
036:
037: public LinkNode getNext() {
038: return next;
039: }
040:
041: public Node getNode() {
042: return node;
043: }
044:
045: public void LinkWith(LinkNode lk) {
046: next = lk;
047: }
048: }
049:
050: /**
051: * DOCUMENT ME!
052: */
053: class Automaton {
054: private LinkNode head;
055: private LinkNode tail;
056: private Node[] equivalence_classes; // array of representatives of equivalent states
057:
058: public Automaton() {
059: head = tail = null;
060: equivalence_classes = null;
061: }
062:
063: public static void FSPoutput(State[] automaton) {
064: boolean comma = false;
065:
066: if (automaton == null) {
067: System.out.println("\n\nRES = STOP.");
068:
069: return;
070: } else {
071: System.out.println("\n\nRES = S0,");
072: }
073:
074: int size = Pool.assign();
075:
076: for (int i = 0; i < size; i++) {
077: if ((automaton[i] != null)
078: && (i == automaton[i].get_representativeId())) // a representative so print
079: {
080: if (comma) {
081: System.out.println("),");
082: }
083:
084: comma = true;
085: System.out.print("S"
086: + automaton[i].get_representativeId());
087: System.out.print("=");
088: automaton[i].FSPoutput();
089: }
090: }
091:
092: System.out.println(").\n");
093: }
094:
095: public static Graph SMoutput(State[] automaton) {
096: Graph g = new Graph();
097: g.setStringAttribute("type", "gba");
098: g.setStringAttribute("ac", "edges");
099:
100: if (automaton == null) {
101: return g;
102: }
103:
104: int size = Pool.assign();
105: gov.nasa.ltl.graph.Node[] nodes = new gov.nasa.ltl.graph.Node[size];
106:
107: for (int i = 0; i < size; i++) {
108: if ((automaton[i] != null)
109: && (i == automaton[i].get_representativeId())) {
110: nodes[i] = new gov.nasa.ltl.graph.Node(g);
111: nodes[i].setStringAttribute("label", "S"
112: + automaton[i].get_representativeId());
113: }
114: }
115:
116: for (int i = 0; i < size; i++) {
117: if ((automaton[i] != null)
118: && (i == automaton[i].get_representativeId())) {
119: automaton[i].SMoutput(nodes, nodes[i]);
120: }
121: }
122:
123: if (Node.accepting_conds == 0) {
124: g.setIntAttribute("nsets", 1);
125: } else {
126: g.setIntAttribute("nsets", Node.accepting_conds);
127: }
128:
129: return g;
130: }
131:
132: public void add(Node nd) {
133: LinkNode newNode = new LinkNode(nd, null);
134:
135: if (head == null) // set is currently empty
136: {
137: head = tail = newNode;
138: } else // put element at end of list
139: {
140: tail.LinkWith(newNode);
141: tail = newNode;
142: }
143: }
144:
145: public Node alreadyThere(Node nd) {
146: /* when running LTL2Buchi is already there if next fields and
147: accepting conditions are the same. For LTL2AUT, old fields
148: also have to be the same
149: */
150: LinkNode nextNd = head;
151:
152: while (nextNd != null) {
153: Node currState = nextNd.getNode();
154:
155: if (currState.getField_next().equals(nd.getField_next())
156: && currState.compare_accepting(nd)
157: && (Translator.get_algorithm() == Translator.LTL2BUCHI || (currState
158: .getField_old().equals(nd.getField_old())))) {
159: //System.out.println("Match found");
160: return currState;
161: } else {
162: nextNd = nextNd.getNext();
163: }
164: }
165:
166: //System.out.println("No match found for node " + nd.getNodeId());
167: return null;
168: }
169:
170: /* public int get_representative_id(int automaton_index, State[] automaton)
171: {
172: return equivalence_classes[automaton[automaton_index].get_equivalence_class()].getNodeId();
173: }
174: */
175: public int index_equivalence(Node nd) {
176: // check if next field of node is already represented
177: int index;
178:
179: for (index = 0; index < Pool.assign(); index++) {
180: if (equivalence_classes[index] == null) {
181: // System.out.println("Null object");
182: break;
183: } else if ((Translator.get_algorithm() == Translator.LTL2BUCHI)
184: && (equivalence_classes[index].getField_next()
185: .equals(nd.getField_next()))) {
186: // System.out.println("Successful merge");
187: return (equivalence_classes[index].getNodeId());
188: }
189: }
190:
191: if (index == Pool.assign()) {
192: System.out
193: .println("ERROR - size of equivalence classes array was incorrect");
194: }
195:
196: equivalence_classes[index] = nd;
197:
198: return (equivalence_classes[index].getNodeId());
199: }
200:
201: public State[] structForRuntAnalysis() {
202: // now also fixes equivalence classes
203: Pool.stop();
204:
205: int automatonSize = Pool.assign();
206: State[] RTstruct = new State[automatonSize];
207: equivalence_classes = new Node[automatonSize];
208:
209: if (head == null) {
210: return RTstruct;
211: }
212:
213: LinkNode nextNd = head;
214: Node current;
215:
216: while (nextNd != null) {
217: current = nextNd.getNode();
218: current.set_equivalenceId(index_equivalence(current));
219: nextNd.getNode().RTstructure(RTstruct);
220: nextNd = nextNd.getNext();
221: }
222:
223: return RTstruct;
224: }
225: }
|