---

LTL2Buchi.java

package gov.nasa.arc.ase.ltl;

/* (c) 2001 Dimitra Giannakopoulou and Flavio Lerda*/


import gov.nasa.arc.ase.util.graph.*;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import java.io.*;

public class LTL2Buchi {
  private static String loadLTL(String fname) {
    try {
      BufferedReader in = new BufferedReader(new FileReader(fname));

      return in.readLine();
    } catch(FileNotFoundException e) {
      throw new JPFErrorException("Can't load LTL formula: " + fname);
    } catch(IOException e) {
      throw new JPFErrorException("Error read on LTL formula: " + fname);
    }
  }  
  public static void main(String[] args) {
    if(args.length > 1) {
      System.out.println("usage:");
      System.out.println("\tjava gov.nasa.arc.ase.ltl.LTL2Buchi [<filename>|<ltl-formula>]");
      return;
    }

    String ltl = null;

    if(args.length == 0)
      ltl = readLTL();
    else {
      ltl = args[0];

      if(ltl.endsWith(".ltl"))
    ltl = loadLTL(ltl);
      else if(ltl.equals("-"))
    ltl = readLTL();
    }

    Graph g = translate(ltl);

    g.save(Graph.FSP_FORMAT);
  }  
  private static String readLTL() {
    try {
      BufferedReader in = new BufferedReader(new InputStreamReader(System.in));

      System.out.print("Insert LTL formula: ");
      return in.readLine();
    } catch(IOException e) {
      throw new JPFErrorException("Invalid LTL formula");
    }
  }  
  public static Graph translate(String formula) {
    try {
      System.out.println("Translating formula: " + formula);
      System.out.println();

      formula = Rewriter.rewrite(formula);
      System.out.println("Rewritten as       : " + formula);
      System.out.println();

      Graph gba = Translator.translate(formula);
//#ifdef BANDERA
      gba.save(System.getProperty("user.dir")+File.separator+"gba.sm");
//#else BANDERA

//#endif BANDERA
      
      System.out.println("Generalized buchi automaton generated: gba.sm");
      System.out.println("\t" + gba.getNodeCount() + " states " + gba.getEdgeCount() + " transitions");
      System.out.println();

      
      /*
      gba = SCCReduction.reduce(gba);
      gba.save("scc-gba.sm");
      System.out.println("Strongly connected component reduction: scc-gba.sm");
      System.out.println("\t" + gba.getNodeCount() + " states " + gba.getEdgeCount() + " transitions");
      System.out.println();
      */

      gba = SuperSetReduction.reduce(gba);
//#ifdef BANDERA
      gba.save(System.getProperty("user.dir")+File.separator+"ssr-gba.sm");
//#else BANDERA

//#endif BANDERA
      System.out.println("Superset reduction: ssr-gba.sm");
      System.out.println("\t" + gba.getNodeCount() + " states " + gba.getEdgeCount() + " transitions");
      System.out.println();

      Graph ba = Degeneralize.degeneralize(gba);
//#ifdef BANDERA
      ba.save(System.getProperty("user.dir")+File.separator+"ba.sm");
//#else BANDERA

//#endif BANDERA
      System.out.println("Degeneralized buchi automaton generated: ba.sm");
      System.out.println("\t" + ba.getNodeCount() + " states " + ba.getEdgeCount() + " transitions");
      System.out.println();

      ba = SCCReduction.reduce(ba);
//#ifdef BANDERA
      ba.save(System.getProperty("user.dir")+File.separator+"scc-ba.sm");
//#else BANDERA

//#endif BANDERA
      System.out.println("Strongly connected component reduction: scc-ba.sm");
      System.out.println("\t" + ba.getNodeCount() + " states " + ba.getEdgeCount() + " transitions");
      System.out.println();
/*
      ba = Simplify.simplify(ba);
//#ifdef BANDERA
      ba.save(System.getProperty("user.dir")+File.separator+"final.sm");
//#else BANDERA

//#endif BANDERA
      System.out.println("Simplification applied: final.sm");
      System.out.println("\t" + ba.getNodeCount() + " states " + ba.getEdgeCount() + " transitions");
      System.out.println();
*/
      
      ba = SFSReduction.reduce(ba);
//#ifdef BANDERA
      ba.save(System.getProperty("user.dir")+File.separator+"scc-ba.sm");
//#else BANDERA

//#endif BANDERA
      System.out.println("Fair simulation applied: fairSim-final.sm");
      System.out.println("\t" + ba.getNodeCount() + " states " + ba.getEdgeCount() + " transitions");
      System.out.println();

      return ba;
    } catch(IOException e) {
      throw new JPFErrorException(e.getMessage());
    }
  }  
}

---