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 SynchronousProduct {
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: boolean b0 = e0.getBooleanAttribute("acc" + i);
056: boolean b1 = e1.getBooleanAttribute("acc" + i);
057:
058: if (b1 && !b0) { // corrected by Dimitra
059: found = false;
060:
061: break;
062: }
063: }
064: }
065:
066: if (found) {
067: theEdge = e1;
068: }
069: }
070:
071: if (theEdge != null) {
072: Node next1 = theEdge.getNext();
073: boolean newNext = isNew(nodes, next0, next1);
074: Node next = get(g, nodes, next0, next1);
075: Edge e = new Edge(n, next, e0.getGuard(), theEdge
076: .getAction(), null);
077:
078: if (newNext) {
079: dfs(g, nodes, nsets, next0, next1);
080: }
081: }
082: }
083: }
084:
085: public static void main(String[] args) {
086: Graph g0;
087: Graph g1;
088:
089: try {
090: g0 = Graph.load(args[0]);
091: g1 = Graph.load(args[1]);
092: } catch (IOException e) {
093: System.err.println("Can't load automata");
094: System.exit(1);
095:
096: return;
097: }
098:
099: Graph g = product(g0, g1);
100:
101: g.save();
102: }
103:
104: public static Graph product(Graph g0, Graph g1) {
105: int nsets = g0.getIntAttribute("nsets");
106:
107: if (nsets != g1.getIntAttribute("nsets")) {
108: System.err.println("Different number of accepting sets");
109: System.exit(1);
110: }
111:
112: Node[][] nodes;
113: Graph g = new Graph();
114: g.setStringAttribute("type", "ba");
115: g.setStringAttribute("ac", "nodes");
116:
117: nodes = new Node[g0.getNodeCount()][g1.getNodeCount()];
118:
119: dfs(g, nodes, nsets, g0.getInit(), g1.getInit());
120:
121: return g;
122: }
123:
124: private static boolean isNew(Node[][] nodes, Node n0, Node n1) {
125: return nodes[n0.getId()][n1.getId()] == null;
126: }
127:
128: private static Node get(Graph g, Node[][] nodes, Node n0, Node n1) {
129: if (nodes[n0.getId()][n1.getId()] == null) {
130: Node n = new Node(g);
131: String label0 = n0.getStringAttribute("label");
132: String label1 = n1.getStringAttribute("label");
133:
134: if (label0 == null) {
135: label0 = Integer.toString(n0.getId());
136: }
137:
138: if (label1 == null) {
139: label1 = Integer.toString(n1.getId());
140: }
141:
142: n.setStringAttribute("label", label0 + "+" + label1);
143:
144: if (n1.getBooleanAttribute("accepting")) {
145: n.setBooleanAttribute("accepting", true);
146: }
147:
148: return nodes[n0.getId()][n1.getId()] = n;
149: }
150:
151: return nodes[n0.getId()][n1.getId()];
152: }
153: }
|