KickJava   Java API By Example, From Geeks To Geeks.

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


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
21 // Written by Dimitra Giannakopoulou, 19 Jan 2001
22 package gov.nasa.ltl.trans;
23
24 import gov.nasa.ltl.graph.*;
25
26 /**
27  * DOCUMENT ME!
28  */
29 public class Translator {
30   public static final int LTL2AUT = 0;
31   public static final int LTL2BUCHI = 1;
32   private static int algorithm = LTL2BUCHI; // by default
33
34   public static int get_algorithm () {
35     return algorithm;
36   }
37
38   public static boolean set_algorithm (int alg) {
39     // returns true iff value was legal
40 if ((alg == LTL2AUT) || (alg == LTL2BUCHI)) {
41       algorithm = alg;
42
43       return true;
44     } else {
45       return false;
46     }
47   }
48
49   public static Graph translate (String JavaDoc formula) {
50     try {
51       Formula ltl = Formula.parse(formula);
52       Node init = Node.createInitial(ltl);
53       State[] states = (init.expand(new Automaton())).structForRuntAnalysis();
54       return Automaton.SMoutput(states);
55     } catch (ParseErrorException e) {
56       throw new LTLErrorException("parse error: " + e.getMessage());
57     }
58   }
59 }
Popular Tags