01: //
02: // Copyright (C) 2005 United States Government as represented by the
03: // Administrator of the National Aeronautics and Space Administration
04: // (NASA). All Rights Reserved.
05: //
06: // This software is distributed under the NASA Open Source Agreement
07: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
08: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: // 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 Giannakopoulou, 19 Jan 2001
21: package gov.nasa.ltl.trans;
22:
23: import gov.nasa.ltl.graph.*;
24:
25: /**
26: * DOCUMENT ME!
27: */
28: public class Translator {
29: public static final int LTL2AUT = 0;
30: public static final int LTL2BUCHI = 1;
31: private static int algorithm = LTL2BUCHI; // by default
32:
33: public static int get_algorithm() {
34: return algorithm;
35: }
36:
37: public static boolean set_algorithm(int alg) {
38: // returns true iff value was legal
39: if ((alg == LTL2AUT) || (alg == LTL2BUCHI)) {
40: algorithm = alg;
41:
42: return true;
43: } else {
44: return false;
45: }
46: }
47:
48: public static Graph translate(String formula) {
49: try {
50: Formula ltl = Formula.parse(formula);
51: Node init = Node.createInitial(ltl);
52: State[] states = (init.expand(new Automaton()))
53: .structForRuntAnalysis();
54: return Automaton.SMoutput(states);
55: } catch (ParseErrorException e) {
56: throw new LTLErrorException("parse error: "
57: + e.getMessage());
58: }
59: }
60: }
|