KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > ltl > trans > Rewriter


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.trans;
21
22 import java.io.*;
23 import java.io.BufferedReader JavaDoc;
24
25 // Added by ckong - Sept 7, 2001
26 import java.io.StringReader JavaDoc;
27
28
29 /**
30  * DOCUMENT ME!
31  */
32 public class Rewriter {
33   public static Formula applyRule (Formula expr, Formula rule,
34                                    Formula rewritten) {
35     return expr.rewrite(rule, rewritten);
36   }
37
38   public static void main (String JavaDoc[] args) {
39     int osize = 0;
40     int rsize = 0;
41
42     try {
43       if (args.length != 0) {
44         for (int i = 0; i < args.length; i++) {
45           Formula f = Formula.parse(args[i]);
46
47           osize += f.size();
48           System.out.println(f = rewrite(f));
49           rsize += f.size();
50
51           System.err.println(((rsize * 100) / osize) + "% (" + osize +
52                              " => " + rsize + ")");
53         }
54       } else {
55         BufferedReader JavaDoc in = new BufferedReader JavaDoc(new InputStreamReader(System.in));
56
57         while (true) {
58           try {
59             String JavaDoc line = in.readLine();
60
61             if (line == null) {
62               break;
63             }
64
65             if (line.equals("")) {
66               continue;
67             }
68
69             Formula f = Formula.parse(line);
70
71             osize += f.size();
72             System.out.println(f = rewrite(f));
73             rsize += f.size();
74
75             System.err.println(((rsize * 100) / osize) + "% (" + osize +
76                                " => " + rsize + ")");
77           } catch (IOException e) {
78             System.out.println("error");
79
80             break;
81           }
82         }
83       }
84     } catch (ParseErrorException e) {
85       System.err.println("parse error: " + e.getMessage());
86     }
87   }
88
89   public static Formula[] readRules () {
90     Formula[] rules = new Formula[0];
91
92     try {
93       // Modified by ckong - Sept 7, 2001
94
95       /*
96          FileReader fr = null;
97          
98                for(int i = 0, l = ClassPath.length(); i < l; i++)
99            try {
100              fr = new FileReader(ClassPath.get(i) + File.separator + "gov.nasa.ltl.trans.rules".replace('.', File.separatorChar));
101            } catch(FileNotFoundException e) {
102            }
103          
104                if(fr == null) {
105            try {
106              fr = new FileReader("rules");
107            } catch(FileNotFoundException e) {
108            }
109                }
110          
111                if(fr == null) return null;
112                
113                BufferedReader in = new BufferedReader(fr);
114        */
115       BufferedReader JavaDoc in = new BufferedReader JavaDoc(
116                                 new StringReader JavaDoc(RulesClass.getRules()));
117
118       while (true) {
119         String JavaDoc line = in.readLine();
120
121         if (line == null) {
122           break;
123         }
124
125         if (line.equals("")) {
126           continue;
127         }
128
129         Formula rule = Formula.parse(line);
130
131         Formula[] n = new Formula[rules.length + 1];
132         System.arraycopy(rules, 0, n, 0, rules.length);
133         n[rules.length] = rule;
134         rules = n;
135       }
136     } catch (IOException e) {
137     } catch (ParseErrorException e) {
138       System.err.println("parse error: " + e.getMessage());
139       System.exit(1);
140     }
141
142     return rules;
143   }
144
145   public static String JavaDoc rewrite (String JavaDoc expr) 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) throws ParseErrorException {
158     // System.out.println("testing if gets in here");
159 Formula[] rules = readRules();
160
161     if (rules == null) {
162       return expr;
163     }
164
165     try {
166       boolean negated = false;
167       boolean changed;
168
169       do {
170         Formula old;
171         changed = false;
172
173         do {
174           old = expr;
175
176           for (int i = 0; i < rules.length; i += 2) {
177             expr = applyRule(expr, rules[i], rules[i + 1]);
178           }
179
180           if (old != expr) {
181             changed = true;
182           }
183         } while (old != expr);
184
185         negated = !negated;
186         expr = Formula.parse("!" + expr.toString());
187       } while (changed || negated);
188
189       return expr;
190     } catch (ParseErrorException e) {
191       throw new ParseErrorException(e.getMessage());
192     }
193   }
194 }
Popular Tags