1 20 package gov.nasa.ltl.trans; 23 24 import gov.nasa.ltl.graph.*; 25 26 import java.io.*; 27 28 31 public class LTL2Buchi { 32 private static boolean debug = false; 33 34 public static void main(String [] args) { 35 String 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 formula, boolean rewrite, 137 boolean bisim, boolean fair_sim) throws ParseErrorException { 138 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 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 } 171 172 188 if (superset) { 189 gba = SuperSetReduction.reduce(gba); 190 191 if (debug) { 192 System.out.println("\n***********************"); 194 System.out.println("Superset reduction"); 195 System.out.println("\t" + gba.getNodeCount() + " states " 196 + gba.getEdgeCount() + " transitions"); 197 198 } 201 } 202 203 Graph ba = Degeneralize.degeneralize(gba); 204 205 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 } 215 216 if (scc) { 217 ba = SCCReduction.reduce(ba); 218 219 if (debug) { 220 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 } 229 } 230 231 if (bisim) { 232 ba = Simplify.simplify(ba); 233 234 if (debug) { 235 System.out.println("\n***********************"); 237 System.out.println("Bisimulation applied"); 238 System.out.println("\t" + ba.getNodeCount() + " states " 239 + ba.getEdgeCount() + " transitions"); 240 241 } 244 } 245 246 if (fair_sim) { 247 ba = SFSReduction.reduce(ba); 248 249 if (debug) { 250 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 } 259 } 260 261 System.out.println("***********************\n"); 262 263 reset_all_static(); 264 265 return ba; 266 } 267 268 public static Graph translate(String formula) throws ParseErrorException { 269 return translate(formula, true, true, true); 271 } 272 273 public static Graph translate(File file) throws ParseErrorException { 274 String formula = ""; 275 276 try { 277 LineNumberReader f = new LineNumberReader(new FileReader(file)); 278 formula = f.readLine().trim(); 279 f.close(); 280 } catch (Exception e) { 281 throw new RuntimeException (e.getMessage()); 282 } 283 284 return translate(formula, true, true, true); 285 } 286 287 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 loadLTL(String 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 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 |