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.trans;
020:
021: import java.io.*;
022: import java.io.BufferedReader;
023:
024: // Added by ckong - Sept 7, 2001
025: import java.io.StringReader;
026:
027: /**
028: * DOCUMENT ME!
029: */
030: public class Rewriter {
031: public static Formula applyRule(Formula expr, Formula rule,
032: Formula rewritten) {
033: return expr.rewrite(rule, rewritten);
034: }
035:
036: public static void main(String[] args) {
037: int osize = 0;
038: int rsize = 0;
039:
040: try {
041: if (args.length != 0) {
042: for (int i = 0; i < args.length; i++) {
043: Formula f = Formula.parse(args[i]);
044:
045: osize += f.size();
046: System.out.println(f = rewrite(f));
047: rsize += f.size();
048:
049: System.err.println(((rsize * 100) / osize) + "% ("
050: + osize + " => " + rsize + ")");
051: }
052: } else {
053: BufferedReader in = new BufferedReader(
054: new InputStreamReader(System.in));
055:
056: while (true) {
057: try {
058: String line = in.readLine();
059:
060: if (line == null) {
061: break;
062: }
063:
064: if (line.equals("")) {
065: continue;
066: }
067:
068: Formula f = Formula.parse(line);
069:
070: osize += f.size();
071: System.out.println(f = rewrite(f));
072: rsize += f.size();
073:
074: System.err.println(((rsize * 100) / osize)
075: + "% (" + osize + " => " + rsize + ")");
076: } catch (IOException e) {
077: System.out.println("error");
078:
079: break;
080: }
081: }
082: }
083: } catch (ParseErrorException e) {
084: System.err.println("parse error: " + e.getMessage());
085: }
086: }
087:
088: public static Formula[] readRules() {
089: Formula[] rules = new Formula[0];
090:
091: try {
092: // Modified by ckong - Sept 7, 2001
093:
094: /*
095: FileReader fr = null;
096:
097: for(int i = 0, l = ClassPath.length(); i < l; i++)
098: try {
099: fr = new FileReader(ClassPath.get(i) + File.separator + "gov.nasa.ltl.trans.rules".replace('.', File.separatorChar));
100: } catch(FileNotFoundException e) {
101: }
102:
103: if(fr == null) {
104: try {
105: fr = new FileReader("rules");
106: } catch(FileNotFoundException e) {
107: }
108: }
109:
110: if(fr == null) return null;
111:
112: BufferedReader in = new BufferedReader(fr);
113: */
114: BufferedReader in = new BufferedReader(new StringReader(
115: RulesClass.getRules()));
116:
117: while (true) {
118: String line = in.readLine();
119:
120: if (line == null) {
121: break;
122: }
123:
124: if (line.equals("")) {
125: continue;
126: }
127:
128: Formula rule = Formula.parse(line);
129:
130: Formula[] n = new Formula[rules.length + 1];
131: System.arraycopy(rules, 0, n, 0, rules.length);
132: n[rules.length] = rule;
133: rules = n;
134: }
135: } catch (IOException e) {
136: } catch (ParseErrorException e) {
137: System.err.println("parse error: " + e.getMessage());
138: System.exit(1);
139: }
140:
141: return rules;
142: }
143:
144: public static String rewrite(String expr)
145: throws ParseErrorException {
146: try {
147: // System.out.println("String is: " + expr);
148: Formula formula = Formula.parse(expr);
149:
150: // System.out.println("And after parsing " + formula.toString());
151: return rewrite(formula).toString();
152: } catch (ParseErrorException e) {
153: throw new ParseErrorException(e.getMessage());
154: }
155: }
156:
157: public static Formula rewrite(Formula expr)
158: throws ParseErrorException {
159: // System.out.println("testing if gets in here");
160: Formula[] rules = readRules();
161:
162: if (rules == null) {
163: return expr;
164: }
165:
166: try {
167: boolean negated = false;
168: boolean changed;
169:
170: do {
171: Formula old;
172: changed = false;
173:
174: do {
175: old = expr;
176:
177: for (int i = 0; i < rules.length; i += 2) {
178: expr = applyRule(expr, rules[i], rules[i + 1]);
179: }
180:
181: if (old != expr) {
182: changed = true;
183: }
184: } while (old != expr);
185:
186: negated = !negated;
187: expr = Formula.parse("!" + expr.toString());
188: } while (changed || negated);
189:
190: return expr;
191: } catch (ParseErrorException e) {
192: throw new ParseErrorException(e.getMessage());
193: }
194: }
195: }
|