KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > graph > degenSynchronousProduct


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 package gov.nasa.ltl.graph;
21
22 import java.io.IOException JavaDoc;
23
24 import java.util.Iterator JavaDoc;
25 import java.util.List JavaDoc;
26
27
28 /**
29  * DOCUMENT ME!
30  */
31 public class degenSynchronousProduct {
32   public static void dfs (Graph g, Node[][] nodes, int nsets, Node n0, Node n1) {
33     Node n = get(g, nodes, n0, n1);
34
35     List JavaDoc t0 = n0.getOutgoingEdges();
36     List JavaDoc t1 = n1.getOutgoingEdges();
37
38     for (Iterator JavaDoc i0 = t0.iterator(); i0.hasNext();) {
39       Edge e0 = (Edge) i0.next();
40       Node next0 = e0.getNext();
41       Edge theEdge = null;
42
43       boolean found = false;
44
45       for (Iterator JavaDoc i1 = t1.iterator(); i1.hasNext() && !found;) {
46         Edge e1 = (Edge) i1.next();
47
48         if (e1.getBooleanAttribute("else")) {
49           if (theEdge == null) {
50             theEdge = e1;
51           }
52         } else {
53           found = true;
54
55           for (int i = 0; i < nsets; i++) {
56             // n1 is the degeneraliser automaton
57 // dimitra's code starts here
58 int n1id = n1.getIntAttribute("lower_bound");
59
60             if (i >= n1id) // ignore bits before lower bound
61 {
62               // dimitra's code ends here
63 boolean b0 = e0.getBooleanAttribute("acc" + i);
64               boolean b1 = e1.getBooleanAttribute("acc" + i);
65
66               if (b0 != b1) {
67                 found = false;
68
69                 break;
70               }
71             }
72           }
73         }
74
75         if (found) {
76           theEdge = e1;
77         }
78       }
79
80       if (theEdge != null) {
81         Node next1 = theEdge.getNext();
82         boolean newNext = isNew(nodes, next0, next1);
83         Node next = get(g, nodes, next0, next1);
84         Edge e = new Edge(n, next, e0.getGuard(), theEdge.getAction(), null);
85
86         if (newNext) {
87           dfs(g, nodes, nsets, next0, next1);
88         }
89       }
90     }
91   }
92
93   public static void main (String JavaDoc[] args) {
94     Graph g0;
95     Graph g1;
96
97     try {
98       g0 = Graph.load(args[0]);
99       g1 = Graph.load(args[1]);
100     } catch (IOException JavaDoc e) {
101       System.err.println("Can't load automata");
102       System.exit(1);
103
104       return;
105     }
106
107     Graph g = product(g0, g1);
108
109     g.save();
110   }
111
112   public static Graph product (Graph g0, Graph g1) {
113     int nsets = g0.getIntAttribute("nsets");
114
115     if (nsets != g1.getIntAttribute("nsets")) {
116       System.err.println("Different number of accepting sets");
117       System.exit(1);
118     }
119
120     Node[][] nodes;
121     Graph g = new Graph();
122     g.setStringAttribute("type", "ba");
123     g.setStringAttribute("ac", "nodes");
124
125     nodes = new Node[g0.getNodeCount()][g1.getNodeCount()];
126
127     dfs(g, nodes, nsets, g0.getInit(), g1.getInit());
128
129     return g;
130   }
131
132   private static boolean isNew (Node[][] nodes, Node n0, Node n1) {
133     return nodes[n0.getId()][n1.getId()] == null;
134   }
135
136   private static Node get (Graph g, Node[][] nodes, Node n0, Node n1) {
137     if (nodes[n0.getId()][n1.getId()] == null) {
138       Node n = new Node(g);
139       String JavaDoc label0 = n0.getStringAttribute("label");
140       String JavaDoc label1 = n1.getStringAttribute("label");
141
142       if (label0 == null) {
143         label0 = Integer.toString(n0.getId());
144       }
145
146       if (label1 == null) {
147         label1 = Integer.toString(n1.getId());
148       }
149
150       n.setStringAttribute("label", label0 + "+" + label1);
151
152       if (n1.getBooleanAttribute("accepting")) {
153         n.setBooleanAttribute("accepting", true);
154       }
155
156       return nodes[n0.getId()][n1.getId()] = n;
157     }
158
159     return nodes[n0.getId()][n1.getId()];
160   }
161 }
Popular Tags