KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > trans > Automaton


1
2 //
3 // Copyright (C) 2005 United States Government as represented by the
4 // Administrator of the National Aeronautics and Space Administration
5 // (NASA). All Rights Reserved.
6 //
7 // This software is distributed under the NASA Open Source Agreement
8 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
9 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
10 // directory tree for the complete NOSA document.
11 //
12 // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
13 // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
14 // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
15 // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
16 // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
17 // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
18 // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
19 //
20
21 // Written by Dimitra Giannakopoulou, 19 Jan 2001
22 package gov.nasa.ltl.trans;
23
24 import gov.nasa.ltl.graph.*;
25
26
27 /**
28  * DOCUMENT ME!
29  */
30 class LinkNode {
31   private Node node;
32   private LinkNode next;
33
34   public LinkNode (Node nd, LinkNode nxt) {
35     node = nd;
36     next = nxt;
37   }
38
39   public LinkNode getNext () {
40     return next;
41   }
42
43   public Node getNode () {
44     return node;
45   }
46
47   public void LinkWith (LinkNode lk) {
48     next = lk;
49   }
50 }
51
52 /**
53  * DOCUMENT ME!
54  */
55 class Automaton {
56   private LinkNode head;
57   private LinkNode tail;
58   private Node[] equivalence_classes; // array of representatives of equivalent states
59
60   public Automaton () {
61     head = tail = null;
62     equivalence_classes = null;
63   }
64
65   public static void FSPoutput (State[] automaton) {
66     boolean comma = false;
67
68     if (automaton == null) {
69       System.out.println("\n\nRES = STOP.");
70
71       return;
72     } else {
73       System.out.println("\n\nRES = S0,");
74     }
75
76     int size = Pool.assign();
77
78     for (int i = 0; i < size; i++) {
79       if ((automaton[i] != null) &&
80               (i == automaton[i].get_representativeId())) // a representative so print
81 {
82         if (comma) {
83           System.out.println("),");
84         }
85
86         comma = true;
87         System.out.print("S" + automaton[i].get_representativeId());
88         System.out.print("=");
89         automaton[i].FSPoutput();
90       }
91     }
92
93     System.out.println(").\n");
94   }
95
96   public static Graph SMoutput (State[] automaton) {
97     Graph g = new Graph();
98     g.setStringAttribute("type", "gba");
99     g.setStringAttribute("ac", "edges");
100
101     if (automaton == null) {
102       return g;
103     }
104
105     int size = Pool.assign();
106     gov.nasa.ltl.graph.Node[] nodes = new gov.nasa.ltl.graph.Node[size];
107
108     for (int i = 0; i < size; i++) {
109       if ((automaton[i] != null) &&
110               (i == automaton[i].get_representativeId())) {
111         nodes[i] = new gov.nasa.ltl.graph.Node(g);
112         nodes[i].setStringAttribute("label",
113                                     "S" +
114                                     automaton[i].get_representativeId());
115       }
116     }
117
118     for (int i = 0; i < size; i++) {
119       if ((automaton[i] != null) &&
120               (i == automaton[i].get_representativeId())) {
121         automaton[i].SMoutput(nodes, nodes[i]);
122       }
123     }
124
125     if (Node.accepting_conds == 0) {
126       g.setIntAttribute("nsets", 1);
127     } else {
128       g.setIntAttribute("nsets", Node.accepting_conds);
129     }
130
131     return g;
132   }
133
134   public void add (Node nd) {
135     LinkNode newNode = new LinkNode(nd, null);
136
137     if (head == null) // set is currently empty
138 {
139       head = tail = newNode;
140     } else // put element at end of list
141 {
142       tail.LinkWith(newNode);
143       tail = newNode;
144     }
145   }
146
147   public Node alreadyThere (Node nd) {
148     /* when running LTL2Buchi is already there if next fields and
149        accepting conditions are the same. For LTL2AUT, old fields
150        also have to be the same
151      */
152     LinkNode nextNd = head;
153
154     while (nextNd != null) {
155       Node currState = nextNd.getNode();
156
157       if (currState.getField_next().equals(nd.getField_next()) &&
158               currState.compare_accepting(nd) &&
159               (Translator.get_algorithm() == Translator.LTL2BUCHI ||
160                 (currState.getField_old().equals(nd.getField_old())))) {
161         //System.out.println("Match found");
162 return currState;
163       } else {
164         nextNd = nextNd.getNext();
165       }
166     }
167
168     //System.out.println("No match found for node " + nd.getNodeId());
169 return null;
170   }
171
172   /* public int get_representative_id(int automaton_index, State[] automaton)
173      {
174      return equivalence_classes[automaton[automaton_index].get_equivalence_class()].getNodeId();
175      }
176    */
177   public int index_equivalence (Node nd) {
178     // check if next field of node is already represented
179 int index;
180
181     for (index = 0; index < Pool.assign(); index++) {
182       if (equivalence_classes[index] == null) {
183         // System.out.println("Null object");
184 break;
185       } else if ((Translator.get_algorithm() == Translator.LTL2BUCHI) &&
186                      (equivalence_classes[index].getField_next().equals(nd.getField_next()))) {
187         // System.out.println("Successful merge");
188 return (equivalence_classes[index].getNodeId());
189       }
190     }
191
192     if (index == Pool.assign()) {
193       System.out.println(
194             "ERROR - size of equivalence classes array was incorrect");
195     }
196
197     equivalence_classes[index] = nd;
198
199     return (equivalence_classes[index].getNodeId());
200   }
201
202   public State[] structForRuntAnalysis () {
203     // now also fixes equivalence classes
204 Pool.stop();
205
206     int automatonSize = Pool.assign();
207     State[] RTstruct = new State[automatonSize];
208     equivalence_classes = new Node[automatonSize];
209
210     if (head == null) {
211       return RTstruct;
212     }
213
214     LinkNode nextNd = head;
215     Node current;
216
217     while (nextNd != null) {
218       current = nextNd.getNode();
219       current.set_equivalenceId(index_equivalence(current));
220       nextNd.getNode().RTstructure(RTstruct);
221       nextNd = nextNd.getNext();
222     }
223
224     return RTstruct;
225   }
226 }
Popular Tags