---

Translator.java

package gov.nasa.arc.ase.ltl;

// Written by Dimitra Giannakopoulou, 19 Jan 2001
import gov.nasa.arc.ase.util.graph.*;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import java.io.*;

public class Translator
{

  public static void main(String[] args) 
  {
    String formula = null;
    String fname = null;

    if(args.length == 2) {
      formula = args[0];
      fname = args[1];
    } else if(args.length == 1) {
      formula = args[0];
    } else {
      BufferedReader input = new BufferedReader(new InputStreamReader(System.in));

      System.out.println("\nPlease enter LTL formula followed by enter");
      try {
    formula = input.readLine();
      } catch (IOException e) {
    System.out.println(" => <input error:" + e.getMessage() + ">");
      }
    }

    if(fname == null)
      translate(formula).save(Graph.FSP_FORMAT);
    else
      try {
    translate(formula).save(fname);
      } catch(IOException e) {
    System.out.println("Can't save file: " + fname);
      }
  }  
  public static Graph translate(String formula) {
    try {
      Formula ltl = Formula.parse(formula);
      Node init = Node.createInitial(ltl);
      State[] states = (init.expand(new Automaton())).structForRuntAnalysis();
      return Automaton.SMoutput(states);
    } catch(ParseErrorException e) {
      throw new JPFErrorException("parse error: " + e.getMessage());
    }
  }  
}

---