KickJava   Java API By Example, From Geeks To Geeks.

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


1 //
2
// Copyright (C) 2005 United States Government as represented by the
3
// Administrator of the National Aeronautics and Space Administration
4
// (NASA). All Rights Reserved.
5
//
6
// This software is distributed under the NASA Open Source Agreement
7
// (NOSA), version 1.3. The NOSA has been approved by the Open Source
8
// Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9
// directory tree for the complete NOSA document.
10
//
11
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18
//
19

20 //Written by Dimitra and Flavio (2001)
21
//Some modifications by: Roby Joehanes
22
package gov.nasa.ltl.trans;
23
24 import gov.nasa.ltl.graph.*;
25
26 import java.io.*;
27
28 /**
29  * DOCUMENT ME!
30  */

31 public class LTL2Buchi {
32     private static boolean debug = false;
33
34     public static void main(String JavaDoc[] args) {
35         String JavaDoc ltl = null;
36         boolean rewrite = true;
37         boolean bisim = true;
38         boolean fairSim = true;
39         boolean file_provided = false;
40         int format = Graph.FSP_FORMAT;
41         debug = true;
42
43         System.out.println("\nAuthors Dimitra Giannakopoulou & Flavio Lerda, \n(c) 2001,2003 NASA Ames Research Center\n");
44
45         Translator.set_algorithm(Translator.LTL2BUCHI);
46
47         if (args.length != 0) {
48             for (int i = 0; i < args.length; i++) {
49                 if (args[i].equals("usage"))
50                     usage_warning();
51                 if (args[i].equals("-a")) {
52                     i++;
53
54                     if (i < args.length) {
55                         if (args[i].equals("ltl2buchi")) {
56                             Translator.set_algorithm(Translator.LTL2BUCHI);
57                         } else if (args[i].equals("ltl2aut")) {
58                             Translator.set_algorithm(Translator.LTL2AUT);
59                         } else {
60                             usage_warning();
61
62                             return;
63                         }
64                     } else {
65                         usage_warning();
66
67                         return;
68                     }
69                 } else if (args[i].equals("-norw")) {
70                     rewrite = false;
71                 } else if (args[i].equals("-nobisim")) {
72                     bisim = false;
73                 } else if (args[i].equals("-nofsim")) {
74                     fairSim = false;
75                 } else if (args[i].equals("-nodebug")) {
76                     debug = false;
77                 } else if (args[i].equals("-o")) {
78                     i++;
79
80                     if (i < args.length) {
81                         if (args[i].equals("fsp"))
82                             format = Graph.FSP_FORMAT;
83                         else if (args[i].equals("promela"))
84                             format = Graph.SPIN_FORMAT;
85                         else if (args[i].equals("xml"))
86                             format = Graph.XML_FORMAT;
87                     }
88
89                 } else if (args[i].equals("-f")) {
90                     i++;
91
92                     if (i < args.length) {
93                         ltl = args[i];
94
95                         if (ltl.endsWith(".ltl")) {
96                             ltl = loadLTL(ltl);
97                             file_provided = true;
98                         } else if (ltl.equals("-")) {
99                         } else {
100                             usage_warning();
101
102                             return;
103                         }
104                     } else {
105                         usage_warning();
106
107                         return;
108                     }
109                 } else {
110                     usage_warning();
111
112                     return;
113                 }
114             }
115         }
116
117         if (!file_provided) {
118             ltl = readLTL();
119         }
120
121         try {
122             Graph g = translate(ltl, rewrite, bisim, fairSim);
123             g.save(format);
124             System.out.println("\n***********************\n");
125         } catch (ParseErrorException ex) {
126             System.out.println("Error: " + ex);
127         }
128     }
129
130     public static void reset_all_static() {
131         Node.reset_static();
132         Formula.reset_static();
133         Pool.reset_static();
134     }
135
136     public static Graph translate(String JavaDoc formula, boolean rewrite,
137             boolean bisim, boolean fair_sim) throws ParseErrorException {
138         // System.out.println("Translating formula: " + formula);
139
// System.out.println();
140
boolean superset = true;
141         boolean scc = true;
142
143         if (rewrite) {
144             try {
145                 formula = Rewriter.rewrite(formula);
146             } catch (ParseErrorException e) {
147                 throw new ParseErrorException(e.getMessage());
148             }
149
150             System.out.println("Rewritten as : " + formula);
151             System.out.println();
152         }
153
154         if (formula == null) {
155             System.out.println("Unexpected null formula");
156         }
157
158         Graph gba = Translator.translate(formula);
159
160         if (debug) {
161             // gba.save("gba.sm");
162
System.out.println("\n***********************");
163             System.out.println("\nGeneralized buchi automaton generated");
164             System.out.println("\t" + gba.getNodeCount() + " states "
165                     + gba.getEdgeCount() + " transitions");
166
167             // System.out.println();
168
// gba.save(Graph.FSP_FORMAT);
169
// System.out.println("***********************\n\n");
170
}
171
172         /*
173          // Omitted - does not seem to always at this stage, for example !(aU (bUc))
174          
175          if (scc)
176          {
177          gba = SCCReduction.reduce(gba);
178          if (debug)
179          {
180          // gba.save("scc-gba.sm");
181          System.out.println("Strongly connected component reduction");
182          System.out.println("\t" + gba.getNodeCount() + " states " + gba.getEdgeCount() + " transitions");
183          System.out.println();
184          gba.save(Graph.FSP_FORMAT);
185          }
186          }
187          */

188         if (superset) {
189             gba = SuperSetReduction.reduce(gba);
190
191             if (debug) {
192                 // gba.save("ssr-gba.sm");
193
System.out.println("\n***********************");
194                 System.out.println("Superset reduction");
195                 System.out.println("\t" + gba.getNodeCount() + " states "
196                         + gba.getEdgeCount() + " transitions");
197
198                 // System.out.println();
199
// gba.save(Graph.FSP_FORMAT);
200
}
201         }
202
203         Graph ba = Degeneralize.degeneralize(gba);
204
205         // ba.save("ba.sm");
206
if (debug) {
207             System.out.println("\n***********************");
208             System.out.println("Degeneralized buchi automaton generated");
209             System.out.println("\t" + ba.getNodeCount() + " states "
210                     + ba.getEdgeCount() + " transitions");
211
212             // System.out.println();
213
// ba.save(Graph.FSP_FORMAT);
214
}
215
216         if (scc) {
217             ba = SCCReduction.reduce(ba);
218
219             if (debug) {
220                 // ba.save("scc-ba.sm");
221
System.out.println("\n***********************");
222                 System.out.println("Strongly connected component reduction");
223                 System.out.println("\t" + ba.getNodeCount() + " states "
224                         + ba.getEdgeCount() + " transitions");
225
226                 // System.out.println();
227
// ba.save(Graph.FSP_FORMAT);
228
}
229         }
230
231         if (bisim) {
232             ba = Simplify.simplify(ba);
233
234             if (debug) {
235                 // ba.save("bisim-final.sm");
236
System.out.println("\n***********************");
237                 System.out.println("Bisimulation applied");
238                 System.out.println("\t" + ba.getNodeCount() + " states "
239                         + ba.getEdgeCount() + " transitions");
240
241                 // System.out.println();
242
// ba.save(Graph.FSP_FORMAT);
243
}
244         }
245
246         if (fair_sim) {
247             ba = SFSReduction.reduce(ba);
248
249             if (debug) {
250                 // ba.save("fairSim-final.sm");
251
System.out.println("\n***********************");
252                 System.out.println("Fair simulation applied");
253                 System.out.println("\t" + ba.getNodeCount() + " states "
254                         + ba.getEdgeCount() + " transitions");
255
256                 // System.out.println();
257
// ba.save(Graph.FSP_FORMAT);
258
}
259         }
260
261         System.out.println("***********************\n");
262
263         reset_all_static();
264
265         return ba;
266     }
267
268     public static Graph translate(String JavaDoc formula) throws ParseErrorException {
269         // To work with Bandera and JPF
270
return translate(formula, true, true, true);
271     }
272
273     public static Graph translate(File file) throws ParseErrorException {
274         String JavaDoc formula = "";
275
276         try {
277             LineNumberReader f = new LineNumberReader(new FileReader(file));
278             formula = f.readLine().trim();
279             f.close();
280         } catch (Exception JavaDoc e) {
281             throw new RuntimeException JavaDoc(e.getMessage());
282         }
283
284         return translate(formula, true, true, true);
285     }
286
287     /**
288      * Commented out on 8/7/03 by Dimitra - apparently redundant now
289      * since JPF not tied with Bandera any longer
290      *
291      *
292      public static Graph translate(String formula) throws ParseErrorException {
293      
294      // To work with Bandera and JPF
295      
296      boolean rewrite = true;
297      boolean superset = true;
298      boolean scc = true;
299      boolean bisim = true;
300      boolean fair_sim = true;
301      
302      if (rewrite) {
303      try {
304      formula = Rewriter.rewrite(formula);
305      } catch (ParseErrorException e) {
306      throw new ParseErrorException(e.getMessage());
307      }
308      System.out.println("Rewritten as : " + formula);
309      System.out.println();
310      }
311      
312      Graph gba = Translator.translate(formula);
313      
314      //#ifdef BANDERA
315      try {
316      gba.save(System.getProperty("user.dir") + File.separator + "gba.sm");
317      } catch (IOException ex) {
318      }
319      
320      //#else BANDERA
321      
322      //#endif BANDERA
323      
324      if (superset) {
325      gba = SuperSetReduction.reduce(gba);
326      
327      //#ifdef BANDERA
328      try {
329      gba.save(
330      System.getProperty("user.dir") + File.separator + "ssr-gba.sm");
331      } catch (IOException ex) {
332      }
333      //#else BANDERA
334      
335      //#endif BANDERA
336      }
337      
338      Graph ba = Degeneralize.degeneralize(gba);
339      
340      //#ifdef BANDERA
341      try {
342      ba.save(System.getProperty("user.dir") + File.separator + "ba.sm");
343      } catch (IOException ex) {
344      }
345      //#else BANDERA
346      
347      //#endif BANDERA
348      
349      if (scc) {
350      ba = SCCReduction.reduce(ba);
351      
352      //#ifdef BANDERA
353      try {
354      ba.save(System.getProperty("user.dir") + File.separator + "scc-ba.sm");
355      } catch (IOException ex) {
356      }
357      //#else BANDERA
358      
359      //#endif BANDERA
360      }
361      
362      if (bisim) {
363      ba = Simplify.simplify(ba);
364      //#ifdef BANDERA
365      try {
366      ba.save(System.getProperty("user.dir") + File.separator + "bisim.sm");
367      } catch (IOException ex) {
368      }
369      //#else BANDERA
370      
371      //#endif BANDERA
372      }
373      
374      if (fair_sim) {
375      ba = SFSReduction.reduce(ba);
376      //#ifdef BANDERA
377      try {
378      ba.save(
379      System.getProperty("user.dir") + File.separator + "fairSim-ba.sm");
380      } catch (IOException ex) {
381      }
382      //#else BANDERA
383      
384      //#endif BANDERA
385      
386      }
387      
388      System.out.println("***********************\n");
389      
390      reset_all_static();
391      return ba;
392      
393      }
394      */

395     public static void usage_warning() {
396         System.out.println("\n******* USAGE *******");
397         System.out.println("java gov.nasa.ltl.trans.LTL2Buchi <options>");
398         System.out.println("\toptions can be (in any order):");
399         System.out
400                 .println("\t\t \"-f <filename.ltl>\" (read formula from file)");
401         System.out
402                 .println("\t\t \"-a [ltl2buchi|ltl2aut]\" (set algorithm to be used)");
403         System.out.println("\t\t \"-norw\" (no rewriting)");
404         System.out.println("\t\t \"-nobisim\" (no bisimulation reduction)");
405         System.out.println("\t\t \"-nofsim\" (no fair simulation reduction)");
406         System.out
407                 .println("\t\t \"-o [fsp|promela|xml>\" (format of output; default is fsp)");
408
409         return;
410     }
411
412     private static String JavaDoc loadLTL(String JavaDoc fname) {
413         try {
414             BufferedReader in = new BufferedReader(new FileReader(fname));
415
416             return in.readLine();
417         } catch (FileNotFoundException e) {
418             throw new LTLErrorException("Can't load LTL formula: " + fname);
419         } catch (IOException e) {
420             throw new LTLErrorException("Error read on LTL formula: " + fname);
421         }
422     }
423
424     private static String JavaDoc readLTL() {
425         try {
426             BufferedReader in = new BufferedReader(new InputStreamReader(
427                     System.in));
428
429             System.out.print("\nInsert LTL formula: ");
430
431             return in.readLine();
432         } catch (IOException e) {
433             throw new LTLErrorException("Invalid LTL formula");
434         }
435     }
436 }
Popular Tags