Browse Source

Add Jltl2baCmdLine command-line interface for LTL -> NBA functionality (for testing)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10534 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
449b06ef8f
  1. 114
      prism/src/jltl2ba/Jltl2baCmdLine.java

114
prism/src/jltl2ba/Jltl2baCmdLine.java

@ -0,0 +1,114 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
//
//------------------------------------------------------------------------------
//
// This file is part of PRISM.
//
// PRISM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// PRISM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with PRISM; if not, write to the Free Software Foundation,
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
//
//==============================================================================
package jltl2ba;
import java.io.BufferedReader;
import java.io.FileReader;
import java.io.InputStreamReader;
import java.io.PrintStream;
import jltl2dstar.NBA;
/**
* Command-line interface to the jltl2ba LTL->NBA translator.
*/
public class Jltl2baCmdLine {
public int run(String formula, PrintStream output) throws Exception {
formula = formula.trim();
SimpleLTL ltl = SimpleLTL.parseFormulaLBT(formula);
ltl = ltl.simplify();
NBA nba = ltl.toNBA();
// nba.print_lbtt(output);
nba.print_hoa(output);
return 0;
}
public static void main(String[] args) {
int rv = 0;
int outfile_pos = 1;
BufferedReader r = null;
try {
String formula;
if (args.length == 0) {
usage("");
}
if (args[0].equals("--ltl")) {
if (args.length <= 1)
usage("Missing formula");
formula = args[1];
outfile_pos++;
} else {
if (args[0].equals("-")) {
r = new BufferedReader(new InputStreamReader(System.in));
} else {
r = new BufferedReader(new FileReader(args[0]));
}
}
if (outfile_pos >= args.length) {
usage("Missing output file");
}
PrintStream output;
String outfile = args[outfile_pos];
if (outfile.equals("-")) {
output = System.out;
} else {
output = new PrintStream(outfile);
}
formula = r.readLine();
r.close();
Jltl2baCmdLine jltl2ba = new Jltl2baCmdLine();
rv = jltl2ba.run(formula, output);
output.close();
} catch (Exception e) {
System.err.println(e.toString());
rv = 1;
}
if (rv != 0) {
System.exit(rv);
}
}
private static void usage(String error)
{
if (!error.isEmpty()) {
System.err.println("Error: " + error);
System.err.println();
}
System.err.println("Usage:");
System.err.println(" --ltl formula out-file");
System.err.println(" or");
System.err.println(" in-file out-file");
System.err.println("\n Filename of '-' stands for standard input/output");
System.exit(1);
}
}
Loading…
Cancel
Save