|
1
2 package gov.nasa.ltl.graph;
21
22 import java.io.*;
23
24 import java.util.BitSet  ;
25 import java.util.Iterator ;
26 import java.util.List ;
27
28
29
32 public class SCCReduction {
33 public static void main (String [] args) {
34 if (args.length > 1) {
35 System.out.println("usage:");
36 System.out.println("\tjava gov.nasa.ltl.graph.SCCReduction [<filename>]");
37
38 return;
39 }
40
41 Graph g = null;
42
43 try {
44 if (args.length == 0) {
45 g = Graph.load();
46 } else {
47 g = Graph.load(args[0]);
48 }
49 } catch (IOException e) {
50 System.out.println("Can't load the graph.");
51
52 return;
53 }
54
55 g = reduce(g);
56
57 g.save();
58 }
59
60 public static Graph reduce (Graph g) {
61 boolean changed;
62 String type = g.getStringAttribute("type");
63 String ac = g.getStringAttribute("ac");
64 boolean acNodes = ac.equals("nodes");
65
66 for (Iterator i = SCC.scc(g).iterator(); i.hasNext();) {
67 clearExternalEdges((List ) i.next(), g);
68 }
69
70 do {
71 changed = false;
72
73 List sccs = SCC.scc(g);
74
75 for (Iterator i = sccs.iterator(); i.hasNext();) {
76 List scc = (List ) i.next();
77 boolean accepting = isAccepting(scc, g);
78
79 if (!accepting && isTerminal(scc)) {
80 changed = true;
81
82 for (Iterator j = scc.iterator(); j.hasNext();) {
83 ((Node) j.next()).remove();
84 }
85 } else if (isTransient(scc) || !accepting) {
86 changed |= anyAcceptingState(scc, g);
87 clearAccepting(scc, g);
88 }
89 }
90 } while (changed);
91
92 return g;
93 }
94
95 private static boolean isAccepting (List scc, Graph g) {
96 String type = g.getStringAttribute("type");
97 String ac = g.getStringAttribute("ac");
98
99 if (type.equals("ba")) {
100 if (ac.equals("nodes")) {
101 for (Iterator i = scc.iterator(); i.hasNext();) {
102 if (((Node) i.next()).getBooleanAttribute("accepting")) {
103 return true;
104 }
105 }
106
107 return false;
108 } else if (ac.equals("edges")) {
109 for (Iterator i = scc.iterator(); i.hasNext();) {
110 Node n = (Node) i.next();
111
112 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
113 Edge e = (Edge) j.next();
114
115 if (e.getBooleanAttribute("accepting")) {
116 return true;
117 }
118 }
119 }
120
121 return false;
122 } else {
123 throw new RuntimeException ("invalid accepting type: " + ac);
124 }
125 } else if (type.equals("gba")) {
126 int nsets = g.getIntAttribute("nsets");
127 BitSet found = new BitSet (nsets);
128 int nsccs = 0;
129
130 if (ac.equals("nodes")) {
131 for (Iterator i = scc.iterator(); i.hasNext();) {
132 Node n = (Node) i.next();
133
134 for (int j = 0; j < nsets; j++) {
135 if (n.getBooleanAttribute("acc" + j)) {
136 if (!found.get(j)) {
137 found.set(j);
138 nsccs++;
139 }
140 }
141 }
142 }
143 } else if (ac.equals("edges")) {
144 for (Iterator i = scc.iterator(); i.hasNext();) {
145 Node n = (Node) i.next();
146
147 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
148 Edge e = (Edge) j.next();
149
150 for (int k = 0; k < nsets; k++) {
151 if (e.getBooleanAttribute("acc" + k)) {
152 if (!found.get(k)) {
153 found.set(k);
154 nsccs++;
155 }
156 }
157 }
158 }
159 }
160 } else {
161 throw new RuntimeException ("invalid accepting type: " + ac);
162 }
163
164 return nsccs == nsets;
165 } else {
166 throw new RuntimeException ("invalid graph type: " + type);
167 }
168 }
169
170 private static boolean isTerminal (List scc) {
171 for (Iterator i = scc.iterator(); i.hasNext();) {
172 Node n = (Node) i.next();
173
174 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
175 if (!scc.contains(((Edge) j.next()).getNext())) {
176 return false;
177 }
178 }
179 }
180
181 return true;
182 }
183
184 private static boolean isTransient (List scc) {
185 if (scc.size() != 1) {
186 return false;
187 }
188
189 Node n = (Node) scc.get(0);
190
191 for (Iterator i = n.getOutgoingEdges().iterator(); i.hasNext();) {
192 if (((Edge) i.next()).getNext() == n) {
193 return false;
194 }
195 }
196
197 return true;
198 }
199
200 private static boolean anyAcceptingState (List scc, Graph g) {
201 String type = g.getStringAttribute("type");
202 String ac = g.getStringAttribute("ac");
203
204 if (type.equals("ba")) {
205 if (ac.equals("nodes")) {
206 for (Iterator i = scc.iterator(); i.hasNext();) {
207 Node n = (Node) i.next();
208
209 if (n.getBooleanAttribute("accepting")) {
210 return true;
211 }
212 }
213 } else if (ac.equals("edges")) {
214 for (Iterator i = scc.iterator(); i.hasNext();) {
215 Node n = (Node) i.next();
216
217 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
218 Edge e = (Edge) j.next();
219
220 if (e.getBooleanAttribute("accepting")) {
221 return true;
222 }
223 }
224 }
225 } else {
226 throw new RuntimeException ("invalid accepting type: " + ac);
227 }
228 } else if (type.equals("gba")) {
229 int nsets = g.getIntAttribute("nsets");
230
231 if (ac.equals("nodes")) {
232 for (Iterator i = scc.iterator(); i.hasNext();) {
233 Node n = (Node) i.next();
234
235 for (int j = 0; j < nsets; j++) {
236 if (n.getBooleanAttribute("acc" + j)) {
237 return true;
238 }
239 }
240 }
241 } else if (ac.equals("edges")) {
242 for (Iterator i = scc.iterator(); i.hasNext();) {
243 Node n = (Node) i.next();
244
245 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
246 Edge e = (Edge) j.next();
247
248 for (int k = 0; k < nsets; k++) {
249 if (e.getBooleanAttribute("acc" + j)) {
250 return true;
251 }
252 }
253 }
254 }
255 } else {
256 throw new RuntimeException ("invalid accepting type: " + ac);
257 }
258 } else {
259 throw new RuntimeException ("invalid graph type: " + type);
260 }
261
262 return false;
263 }
264
265 private static void clearAccepting (List scc, Graph g) {
266 String type = g.getStringAttribute("type");
267 String ac = g.getStringAttribute("ac");
268
269 if (type.equals("ba")) {
270 if (ac.equals("nodes")) {
271 for (Iterator i = scc.iterator(); i.hasNext();) {
272 Node n = (Node) i.next();
273
274 n.setBooleanAttribute("accepting", false);
275 }
276 } else if (ac.equals("edges")) {
277 for (Iterator i = scc.iterator(); i.hasNext();) {
278 Node n = (Node) i.next();
279
280 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
281 Edge e = (Edge) j.next();
282
283 e.setBooleanAttribute("accepting", false);
284 }
285 }
286 } else {
287 throw new RuntimeException ("invalid accepting type: " + ac);
288 }
289 } else if (type.equals("gba")) {
290 int nsets = g.getIntAttribute("nsets");
291
292 if (ac.equals("nodes")) {
293 for (Iterator i = scc.iterator(); i.hasNext();) {
294 Node n = (Node) i.next();
295
296 for (int j = 0; j < nsets; j++) {
297 n.setBooleanAttribute("acc" + j, false);
298 }
299 }
300 } else if (ac.equals("edges")) {
301 for (Iterator i = scc.iterator(); i.hasNext();) {
302 Node n = (Node) i.next();
303
304 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
305 Edge e = (Edge) j.next();
306
307 for (int k = 0; k < nsets; k++) {
308 e.setBooleanAttribute("acc" + k, false);
309 }
310 }
311 }
312 } else {
313 throw new RuntimeException ("invalid accepting type: " + ac);
314 }
315 } else {
316 throw new RuntimeException ("invalid graph type: " + type);
317 }
318 }
319
320 private static void clearExternalEdges (List scc, Graph g) {
321 String type = g.getStringAttribute("type");
322 String ac = g.getStringAttribute("ac");
323
324 if (type.equals("ba")) {
325 if (ac.equals("nodes")) {
326 } else if (ac.equals("edges")) {
327 for (Iterator i = scc.iterator(); i.hasNext();) {
328 Node n = (Node) i.next();
329
330 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
331 Edge e = (Edge) j.next();
332
333 if (!scc.contains(e.getNext())) {
334 e.setBooleanAttribute("accepting", false);
335 }
336 }
337 }
338 } else {
339 throw new RuntimeException ("invalid accepting type: " + ac);
340 }
341 } else if (type.equals("gba")) {
342 int nsets = g.getIntAttribute("nsets");
343
344 if (ac.equals("nodes")) {
345 } else if (ac.equals("edges")) {
346 for (Iterator i = scc.iterator(); i.hasNext();) {
347 Node n = (Node) i.next();
348
349 for (Iterator j = n.getOutgoingEdges().iterator(); j.hasNext();) {
350 Edge e = (Edge) j.next();
351
352 if (!scc.contains(e.getNext())) {
353 for (int k = 0; k < nsets; k++) {
354 e.setBooleanAttribute("acc" + k, false);
355 }
356 }
357 }
358 }
359 } else {
360 throw new RuntimeException ("invalid accepting type: " + ac);
361 }
362 } else {
363 throw new RuntimeException ("invalid graph type: " + type);
364 }
365 }
366 } |
Popular Tags |
Java API By Example, From Geeks To Geeks.