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: package gov.nasa.ltl.graph;
020:
021: import java.io.IOException;
022:
023: import java.util.Iterator;
024: import java.util.List;
025:
026: /**
027: * DOCUMENT ME!
028: */
029: public class degenSynchronousProduct {
030: public static void dfs(Graph g, Node[][] nodes, int nsets, Node n0,
031: Node n1) {
032: Node n = get(g, nodes, n0, n1);
033:
034: List t0 = n0.getOutgoingEdges();
035: List t1 = n1.getOutgoingEdges();
036:
037: for (Iterator i0 = t0.iterator(); i0.hasNext();) {
038: Edge e0 = (Edge) i0.next();
039: Node next0 = e0.getNext();
040: Edge theEdge = null;
041:
042: boolean found = false;
043:
044: for (Iterator i1 = t1.iterator(); i1.hasNext() && !found;) {
045: Edge e1 = (Edge) i1.next();
046:
047: if (e1.getBooleanAttribute("else")) {
048: if (theEdge == null) {
049: theEdge = e1;
050: }
051: } else {
052: found = true;
053:
054: for (int i = 0; i < nsets; i++) {
055: // n1 is the degeneraliser automaton
056: // dimitra's code starts here
057: int n1id = n1.getIntAttribute("lower_bound");
058:
059: if (i >= n1id) // ignore bits before lower bound
060: {
061: // dimitra's code ends here
062: boolean b0 = e0.getBooleanAttribute("acc"
063: + i);
064: boolean b1 = e1.getBooleanAttribute("acc"
065: + i);
066:
067: if (b0 != b1) {
068: found = false;
069:
070: break;
071: }
072: }
073: }
074: }
075:
076: if (found) {
077: theEdge = e1;
078: }
079: }
080:
081: if (theEdge != null) {
082: Node next1 = theEdge.getNext();
083: boolean newNext = isNew(nodes, next0, next1);
084: Node next = get(g, nodes, next0, next1);
085: Edge e = new Edge(n, next, e0.getGuard(), theEdge
086: .getAction(), null);
087:
088: if (newNext) {
089: dfs(g, nodes, nsets, next0, next1);
090: }
091: }
092: }
093: }
094:
095: public static void main(String[] args) {
096: Graph g0;
097: Graph g1;
098:
099: try {
100: g0 = Graph.load(args[0]);
101: g1 = Graph.load(args[1]);
102: } catch (IOException e) {
103: System.err.println("Can't load automata");
104: System.exit(1);
105:
106: return;
107: }
108:
109: Graph g = product(g0, g1);
110:
111: g.save();
112: }
113:
114: public static Graph product(Graph g0, Graph g1) {
115: int nsets = g0.getIntAttribute("nsets");
116:
117: if (nsets != g1.getIntAttribute("nsets")) {
118: System.err.println("Different number of accepting sets");
119: System.exit(1);
120: }
121:
122: Node[][] nodes;
123: Graph g = new Graph();
124: g.setStringAttribute("type", "ba");
125: g.setStringAttribute("ac", "nodes");
126:
127: nodes = new Node[g0.getNodeCount()][g1.getNodeCount()];
128:
129: dfs(g, nodes, nsets, g0.getInit(), g1.getInit());
130:
131: return g;
132: }
133:
134: private static boolean isNew(Node[][] nodes, Node n0, Node n1) {
135: return nodes[n0.getId()][n1.getId()] == null;
136: }
137:
138: private static Node get(Graph g, Node[][] nodes, Node n0, Node n1) {
139: if (nodes[n0.getId()][n1.getId()] == null) {
140: Node n = new Node(g);
141: String label0 = n0.getStringAttribute("label");
142: String label1 = n1.getStringAttribute("label");
143:
144: if (label0 == null) {
145: label0 = Integer.toString(n0.getId());
146: }
147:
148: if (label1 == null) {
149: label1 = Integer.toString(n1.getId());
150: }
151:
152: n.setStringAttribute("label", label0 + "+" + label1);
153:
154: if (n1.getBooleanAttribute("accepting")) {
155: n.setBooleanAttribute("accepting", true);
156: }
157:
158: return nodes[n0.getId()][n1.getId()] = n;
159: }
160:
161: return nodes[n0.getId()][n1.getId()];
162: }
163: }
|