From f4381d59ce686d183c72d9c2411e7733166f1854 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Sep 2012 21:44:58 +0200 Subject: [PATCH] Add option --lbt-input to ltl2tgba. Factor it with ltlfilt. * src/bin/ltlfilt.cc: Extra input options into... * src/bin/common_finput.cc, src/bin/common_finput.hh: ... these new files... * src/bin/ltl2tgba.cc: ... and use them here. * src/bin/Makefile.am: Adjust. --- src/bin/Makefile.am | 2 ++ src/bin/common_finput.cc | 71 ++++++++++++++++++++++++++++++++++++++++ src/bin/common_finput.hh | 54 ++++++++++++++++++++++++++++++ src/bin/ltl2tgba.cc | 29 +++++----------- src/bin/ltlfilt.cc | 45 ++++--------------------- 5 files changed, 142 insertions(+), 59 deletions(-) create mode 100644 src/bin/common_finput.cc create mode 100644 src/bin/common_finput.hh diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 471dc1fb1..884b61045 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -30,6 +30,8 @@ noinst_LIBRARIES = libcommon.a libcommon_a_SOURCES = \ common_cout.hh \ common_cout.cc \ + common_finput.cc \ + common_finput.hh \ common_output.cc \ common_output.hh \ common_range.cc \ diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc new file mode 100644 index 000000000..bd6f92803 --- /dev/null +++ b/src/bin/common_finput.cc @@ -0,0 +1,71 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot 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. +// +// Spot 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "common_finput.hh" +#include "error.h" + +#define OPT_LBT 1 + +jobs_t jobs; +bool lbt_input = false; + +static const argp_option options[] = + { + { 0, 0, 0, 0, "Input options:", 1 }, + { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, + { "file", 'F', "FILENAME", 0, + "process each line of FILENAME as a formula", 0 }, + { "lbt-input", OPT_LBT, 0, 0, + "read all formulas using LBT's prefix syntax", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + +const struct argp finput_argp = { options, parse_opt_finput, 0, 0, 0, 0, 0 }; + +int +parse_opt_finput(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case 'f': + jobs.push_back(job(arg, false)); + break; + case 'F': + jobs.push_back(job(arg, true)); + break; + case OPT_LBT: + lbt_input = true; + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +const spot::ltl::formula* +parse_formula(const std::string& s, spot::ltl::parse_error_list& pel) +{ + if (lbt_input) + return spot::ltl::parse_lbt(s, pel); + else + return spot::ltl::parse(s, pel); +} diff --git a/src/bin/common_finput.hh b/src/bin/common_finput.hh new file mode 100644 index 000000000..166cf6fa7 --- /dev/null +++ b/src/bin/common_finput.hh @@ -0,0 +1,54 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot 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. +// +// Spot 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_BIN_COMMON_FINPUT_HH +#define SPOT_BIN_COMMON_FINPUT_HH + +#include "common_sys.hh" + +#include +#include +#include "ltlparse/public.hh" + +struct job +{ + const char* str; + bool file_p; // true if str is a filename, false if it is a formula + + job(const char* str, bool file_p) + : str(str), file_p(file_p) + { + } +}; + +typedef std::vector jobs_t; +extern jobs_t jobs; +extern bool lbt_input; + +extern const struct argp finput_argp; + +int parse_opt_finput(int key, char* arg, struct argp_state* state); + +const spot::ltl::formula* +parse_formula(const std::string& s, spot::ltl::parse_error_list& error_list); + + +#endif // SPOT_BIN_COMMON_FINPUT_HH diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 1f6c855ee..2adf7bc68 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -32,6 +32,7 @@ #include "common_r.hh" #include "common_cout.hh" +#include "common_finput.hh" #include "misc/_config.h" #include "ltlparse/public.hh" @@ -73,11 +74,6 @@ If multiple formulas are supplied, several automata will be output."; static const argp_option options[] = { /**************************************************/ - { 0, 0, 0, 0, "Input options:", 1 }, - { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, - { "file", 'F', "FILENAME", 0, - "process each line of FILENAME as a formula", 0 }, - /**************************************************/ { 0, 0, 0, 0, "Automaton type:", 2 }, { "tgba", OPT_TGBA, 0, 0, "Transition-based Generalized Büchi Automaton (default)", 0 }, @@ -106,19 +102,11 @@ static const argp_option options[] = { 0, 0, 0, 0, 0, 0 } }; -struct job -{ - const char* str; - bool file_p; // true if str is a filename, false if it is a formula - - job(const char* str, bool file_p) - : str(str), file_p(file_p) +const struct argp_child children[] = { - } -}; - -typedef std::vector jobs_t; -static jobs_t jobs; + { &finput_argp, 0, 0, 1 }, + { 0, 0, 0, 0 } + }; spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_pref pref = spot::postprocessor::Small; @@ -214,7 +202,7 @@ namespace const char* filename = 0, int linenum = 0) { spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = spot::ltl::parse(input, pel); + const spot::ltl::formula* f = parse_formula(input, pel); if (!f || pel.size() > 0) { @@ -252,7 +240,8 @@ namespace switch (format) { case Dot: - spot::dotty_reachable(std::cout, aut, type == spot::postprocessor::BA); + spot::dotty_reachable(std::cout, aut, + type == spot::postprocessor::BA); break; case Lbtt: spot::lbtt_reachable(std::cout, aut); @@ -331,7 +320,7 @@ main(int argc, char** argv) argv[0] = const_cast(program_name); const argp ap = { options, parse_opt, "[FORMULA...]", - argp_program_doc, 0, 0, 0 }; + argp_program_doc, children, 0, 0 }; if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) exit(err); diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 01aadc36d..3738afd55 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -31,13 +31,13 @@ #include "progname.h" #include "error.h" +#include "common_finput.hh" #include "common_output.hh" #include "common_cout.hh" #include "common_r.hh" #include "misc/_config.h" #include "misc/hash.hh" -#include "ltlparse/public.hh" #include "ltlvisit/simplify.hh" #include "ltlvisit/length.hh" #include "ltlvisit/relabel.hh" @@ -89,19 +89,12 @@ Exit status:\n\ #define OPT_IMPLIED_BY 23 #define OPT_IMPLY 24 #define OPT_EQUIVALENT_TO 25 -#define OPT_LBT 26 -#define OPT_RELABEL 27 -#define OPT_REMOVE_WM 28 +#define OPT_RELABEL 26 +#define OPT_REMOVE_WM 27 static const argp_option options[] = { /**************************************************/ - { 0, 0, 0, 0, "Input options:", 1 }, - { "formula", 'f', "STRING", 0, "process the formula STRING", 0 }, - { "file", 'F', "FILENAME", 0, - "process each line of FILENAME as a formula", 0 }, - { "lbt-input", OPT_LBT, 0, 0, - "read all formulas using LBT's prefix syntax", 0 }, { 0, 0, 0, 0, "Error handling:", 2 }, { "skip-errors", OPT_SKIP_ERRORS, 0, 0, "output erroneous lines as-is without processing", 0 }, @@ -169,29 +162,15 @@ static const argp_option options[] = const struct argp_child children[] = { + { &finput_argp, 0, 0, 1 }, { &output_argp, 0, 0, -20 }, { 0, 0, 0, 0 } }; -struct job -{ - const char* str; - bool file_p; // true if str is a filename, false if it is a formula - - job(const char* str, bool file_p) - : str(str), file_p(file_p) - { - } -}; - -typedef std::vector jobs_t; -static jobs_t jobs; - static bool one_match = false; enum error_style_t { drop_errors, skip_errors }; static error_style_t error_style = drop_errors; -static bool lbt = false; static bool quiet = false; static bool nnf = false; static bool negate = false; @@ -238,7 +217,7 @@ static const spot::ltl::formula* parse_formula_arg(const std::string& input) { spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = spot::ltl::parse(input, pel); + const spot::ltl::formula* f = parse_formula(input, pel); if (spot::ltl::format_parse_errors(std::cerr, input, pel)) error(2, 0, "parse error when parsing an argument"); return f; @@ -252,12 +231,6 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { - case 'f': - jobs.push_back(job(arg, false)); - break; - case 'F': - jobs.push_back(job(arg, true)); - break; case 'n': negate = true; break; @@ -315,8 +288,6 @@ parse_opt(int key, char* arg, struct argp_state*) spot::ltl::multop::instance(spot::ltl::multop::And, imply, i); break; } - case OPT_LBT: - lbt = true; case OPT_LTL: ltl = true; break; @@ -398,11 +369,7 @@ namespace const char* filename = 0, int linenum = 0) { spot::ltl::parse_error_list pel; - const spot::ltl::formula* f; - if (lbt) - f = spot::ltl::parse_lbt(input, pel); - else - f = spot::ltl::parse(input, pel); + const spot::ltl::formula* f = parse_formula(input, pel); if (!f || pel.size() > 0) {