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:
020: //Written by Dimitra and Flavio (2001)
021: //Some modifications by: Roby Joehanes
022: package gov.nasa.ltl.trans;
023:
024: import gov.nasa.ltl.graph.*;
025:
026: import java.io.*;
027:
028: /**
029: * DOCUMENT ME!
030: */
031: public class LTL2Buchi {
032: private static boolean debug = false;
033:
034: public static void main(String[] args) {
035: String ltl = null;
036: boolean rewrite = true;
037: boolean bisim = true;
038: boolean fairSim = true;
039: boolean file_provided = false;
040: int format = Graph.FSP_FORMAT;
041: debug = true;
042:
043: System.out
044: .println("\nAuthors Dimitra Giannakopoulou & Flavio Lerda, \n(c) 2001,2003 NASA Ames Research Center\n");
045:
046: Translator.set_algorithm(Translator.LTL2BUCHI);
047:
048: if (args.length != 0) {
049: for (int i = 0; i < args.length; i++) {
050: if (args[i].equals("usage"))
051: usage_warning();
052: if (args[i].equals("-a")) {
053: i++;
054:
055: if (i < args.length) {
056: if (args[i].equals("ltl2buchi")) {
057: Translator
058: .set_algorithm(Translator.LTL2BUCHI);
059: } else if (args[i].equals("ltl2aut")) {
060: Translator
061: .set_algorithm(Translator.LTL2AUT);
062: } else {
063: usage_warning();
064:
065: return;
066: }
067: } else {
068: usage_warning();
069:
070: return;
071: }
072: } else if (args[i].equals("-norw")) {
073: rewrite = false;
074: } else if (args[i].equals("-nobisim")) {
075: bisim = false;
076: } else if (args[i].equals("-nofsim")) {
077: fairSim = false;
078: } else if (args[i].equals("-nodebug")) {
079: debug = false;
080: } else if (args[i].equals("-o")) {
081: i++;
082:
083: if (i < args.length) {
084: if (args[i].equals("fsp"))
085: format = Graph.FSP_FORMAT;
086: else if (args[i].equals("promela"))
087: format = Graph.SPIN_FORMAT;
088: else if (args[i].equals("xml"))
089: format = Graph.XML_FORMAT;
090: }
091:
092: } else if (args[i].equals("-f")) {
093: i++;
094:
095: if (i < args.length) {
096: ltl = args[i];
097:
098: if (ltl.endsWith(".ltl")) {
099: ltl = loadLTL(ltl);
100: file_provided = true;
101: } else if (ltl.equals("-")) {
102: } else {
103: usage_warning();
104:
105: return;
106: }
107: } else {
108: usage_warning();
109:
110: return;
111: }
112: } else {
113: usage_warning();
114:
115: return;
116: }
117: }
118: }
119:
120: if (!file_provided) {
121: ltl = readLTL();
122: }
123:
124: try {
125: Graph g = translate(ltl, rewrite, bisim, fairSim);
126: g.save(format);
127: System.out.println("\n***********************\n");
128: } catch (ParseErrorException ex) {
129: System.out.println("Error: " + ex);
130: }
131: }
132:
133: public static void reset_all_static() {
134: Node.reset_static();
135: Formula.reset_static();
136: Pool.reset_static();
137: }
138:
139: public static Graph translate(String formula, boolean rewrite,
140: boolean bisim, boolean fair_sim) throws ParseErrorException {
141: // System.out.println("Translating formula: " + formula);
142: // System.out.println();
143: boolean super set = true;
144: boolean scc = true;
145:
146: if (rewrite) {
147: try {
148: formula = Rewriter.rewrite(formula);
149: } catch (ParseErrorException e) {
150: throw new ParseErrorException(e.getMessage());
151: }
152:
153: System.out.println("Rewritten as : " + formula);
154: System.out.println();
155: }
156:
157: if (formula == null) {
158: System.out.println("Unexpected null formula");
159: }
160:
161: Graph gba = Translator.translate(formula);
162:
163: if (debug) {
164: // gba.save("gba.sm");
165: System.out.println("\n***********************");
166: System.out
167: .println("\nGeneralized buchi automaton generated");
168: System.out.println("\t" + gba.getNodeCount() + " states "
169: + gba.getEdgeCount() + " transitions");
170:
171: // System.out.println();
172: // gba.save(Graph.FSP_FORMAT);
173: // System.out.println("***********************\n\n");
174: }
175:
176: /*
177: // Omitted - does not seem to always at this stage, for example !(aU (bUc))
178:
179: if (scc)
180: {
181: gba = SCCReduction.reduce(gba);
182: if (debug)
183: {
184: // gba.save("scc-gba.sm");
185: System.out.println("Strongly connected component reduction");
186: System.out.println("\t" + gba.getNodeCount() + " states " + gba.getEdgeCount() + " transitions");
187: System.out.println();
188: gba.save(Graph.FSP_FORMAT);
189: }
190: }
191: */
192: if (super set) {
193: gba = SuperSetReduction.reduce(gba);
194:
195: if (debug) {
196: // gba.save("ssr-gba.sm");
197: System.out.println("\n***********************");
198: System.out.println("Superset reduction");
199: System.out.println("\t" + gba.getNodeCount()
200: + " states " + gba.getEdgeCount()
201: + " transitions");
202:
203: // System.out.println();
204: // gba.save(Graph.FSP_FORMAT);
205: }
206: }
207:
208: Graph ba = Degeneralize.degeneralize(gba);
209:
210: // ba.save("ba.sm");
211: if (debug) {
212: System.out.println("\n***********************");
213: System.out
214: .println("Degeneralized buchi automaton generated");
215: System.out.println("\t" + ba.getNodeCount() + " states "
216: + ba.getEdgeCount() + " transitions");
217:
218: // System.out.println();
219: // ba.save(Graph.FSP_FORMAT);
220: }
221:
222: if (scc) {
223: ba = SCCReduction.reduce(ba);
224:
225: if (debug) {
226: // ba.save("scc-ba.sm");
227: System.out.println("\n***********************");
228: System.out
229: .println("Strongly connected component reduction");
230: System.out.println("\t" + ba.getNodeCount()
231: + " states " + ba.getEdgeCount()
232: + " transitions");
233:
234: // System.out.println();
235: // ba.save(Graph.FSP_FORMAT);
236: }
237: }
238:
239: if (bisim) {
240: ba = Simplify.simplify(ba);
241:
242: if (debug) {
243: // ba.save("bisim-final.sm");
244: System.out.println("\n***********************");
245: System.out.println("Bisimulation applied");
246: System.out.println("\t" + ba.getNodeCount()
247: + " states " + ba.getEdgeCount()
248: + " transitions");
249:
250: // System.out.println();
251: // ba.save(Graph.FSP_FORMAT);
252: }
253: }
254:
255: if (fair_sim) {
256: ba = SFSReduction.reduce(ba);
257:
258: if (debug) {
259: // ba.save("fairSim-final.sm");
260: System.out.println("\n***********************");
261: System.out.println("Fair simulation applied");
262: System.out.println("\t" + ba.getNodeCount()
263: + " states " + ba.getEdgeCount()
264: + " transitions");
265:
266: // System.out.println();
267: // ba.save(Graph.FSP_FORMAT);
268: }
269: }
270:
271: System.out.println("***********************\n");
272:
273: reset_all_static();
274:
275: return ba;
276: }
277:
278: public static Graph translate(String formula)
279: throws ParseErrorException {
280: // To work with Bandera and JPF
281: return translate(formula, true, true, true);
282: }
283:
284: public static Graph translate(File file) throws ParseErrorException {
285: String formula = "";
286:
287: try {
288: LineNumberReader f = new LineNumberReader(new FileReader(
289: file));
290: formula = f.readLine().trim();
291: f.close();
292: } catch (Exception e) {
293: throw new RuntimeException(e.getMessage());
294: }
295:
296: return translate(formula, true, true, true);
297: }
298:
299: /**
300: * Commented out on 8/7/03 by Dimitra - apparently redundant now
301: * since JPF not tied with Bandera any longer
302: *
303: *
304: public static Graph translate(String formula) throws ParseErrorException {
305:
306: // To work with Bandera and JPF
307:
308: boolean rewrite = true;
309: boolean superset = true;
310: boolean scc = true;
311: boolean bisim = true;
312: boolean fair_sim = true;
313:
314: if (rewrite) {
315: try {
316: formula = Rewriter.rewrite(formula);
317: } catch (ParseErrorException e) {
318: throw new ParseErrorException(e.getMessage());
319: }
320: System.out.println("Rewritten as : " + formula);
321: System.out.println();
322: }
323:
324: Graph gba = Translator.translate(formula);
325:
326: //#ifdef BANDERA
327: try {
328: gba.save(System.getProperty("user.dir") + File.separator + "gba.sm");
329: } catch (IOException ex) {
330: }
331:
332: //#else BANDERA
333:
334: //#endif BANDERA
335:
336: if (superset) {
337: gba = SuperSetReduction.reduce(gba);
338:
339: //#ifdef BANDERA
340: try {
341: gba.save(
342: System.getProperty("user.dir") + File.separator + "ssr-gba.sm");
343: } catch (IOException ex) {
344: }
345: //#else BANDERA
346:
347: //#endif BANDERA
348: }
349:
350: Graph ba = Degeneralize.degeneralize(gba);
351:
352: //#ifdef BANDERA
353: try {
354: ba.save(System.getProperty("user.dir") + File.separator + "ba.sm");
355: } catch (IOException ex) {
356: }
357: //#else BANDERA
358:
359: //#endif BANDERA
360:
361: if (scc) {
362: ba = SCCReduction.reduce(ba);
363:
364: //#ifdef BANDERA
365: try {
366: ba.save(System.getProperty("user.dir") + File.separator + "scc-ba.sm");
367: } catch (IOException ex) {
368: }
369: //#else BANDERA
370:
371: //#endif BANDERA
372: }
373:
374: if (bisim) {
375: ba = Simplify.simplify(ba);
376: //#ifdef BANDERA
377: try {
378: ba.save(System.getProperty("user.dir") + File.separator + "bisim.sm");
379: } catch (IOException ex) {
380: }
381: //#else BANDERA
382:
383: //#endif BANDERA
384: }
385:
386: if (fair_sim) {
387: ba = SFSReduction.reduce(ba);
388: //#ifdef BANDERA
389: try {
390: ba.save(
391: System.getProperty("user.dir") + File.separator + "fairSim-ba.sm");
392: } catch (IOException ex) {
393: }
394: //#else BANDERA
395:
396: //#endif BANDERA
397:
398: }
399:
400: System.out.println("***********************\n");
401:
402: reset_all_static();
403: return ba;
404:
405: }
406: */
407: public static void usage_warning() {
408: System.out.println("\n******* USAGE *******");
409: System.out
410: .println("java gov.nasa.ltl.trans.LTL2Buchi <options>");
411: System.out.println("\toptions can be (in any order):");
412: System.out
413: .println("\t\t \"-f <filename.ltl>\" (read formula from file)");
414: System.out
415: .println("\t\t \"-a [ltl2buchi|ltl2aut]\" (set algorithm to be used)");
416: System.out.println("\t\t \"-norw\" (no rewriting)");
417: System.out
418: .println("\t\t \"-nobisim\" (no bisimulation reduction)");
419: System.out
420: .println("\t\t \"-nofsim\" (no fair simulation reduction)");
421: System.out
422: .println("\t\t \"-o [fsp|promela|xml>\" (format of output; default is fsp)");
423:
424: return;
425: }
426:
427: private static String loadLTL(String fname) {
428: try {
429: BufferedReader in = new BufferedReader(
430: new FileReader(fname));
431:
432: return in.readLine();
433: } catch (FileNotFoundException e) {
434: throw new LTLErrorException("Can't load LTL formula: "
435: + fname);
436: } catch (IOException e) {
437: throw new LTLErrorException("Error read on LTL formula: "
438: + fname);
439: }
440: }
441:
442: private static String readLTL() {
443: try {
444: BufferedReader in = new BufferedReader(
445: new InputStreamReader(System.in));
446:
447: System.out.print("\nInsert LTL formula: ");
448:
449: return in.readLine();
450: } catch (IOException e) {
451: throw new LTLErrorException("Invalid LTL formula");
452: }
453: }
454: }
|