diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 4094633d7..8fc903e44 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -25,5 +25,7 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a bin_PROGRAMS = ltlfilt genltl -ltlfilt_SOURCES = ltlfilt.cc -genltl_SOURCES = genltl.cc +ltlfilt_SOURCES = ltlfilt.cc common_output.cc +genltl_SOURCES = genltl.cc common_output.cc + +noinst_HEADERS = common_output.hh diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc new file mode 100644 index 000000000..6ffa23a4f --- /dev/null +++ b/src/bin/common_output.cc @@ -0,0 +1,82 @@ +// -*- 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_output.hh" +#include + +#define OPT_SPOT 1 + +output_format_t output_format = spot_output; +bool full_parenth = false; + +static const argp_option options[] = + { + { "full-parentheses", 'p', 0, 0, + "output fully-parenthesized formulas", -20 }, + { "spin", 's', 0, 0, "output in Spin's syntax", -20 }, + { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", -20 }, + { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 }, + { 0, 0, 0, 0, 0, 0 } + }; + +const struct argp output_argp = { options, parse_opt_output, 0, 0, 0, 0, 0 }; + +int +parse_opt_output(int key, char*, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case '8': + output_format = utf8_output; + break; + case 'p': + full_parenth = true; + break; + case 's': + output_format = spin_output; + break; + case OPT_SPOT: + output_format = spot_output; + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +void +output_formula(const spot::ltl::formula* f) +{ + switch (output_format) + { + case spot_output: + spot::ltl::to_string(f, std::cout, full_parenth); + break; + case spin_output: + spot::ltl::to_spin_string(f, std::cout, full_parenth); + break; + case utf8_output: + spot::ltl::to_utf8_string(f, std::cout, full_parenth); + break; + } + std::cout << "\n"; +} diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh new file mode 100644 index 000000000..fec869ad1 --- /dev/null +++ b/src/bin/common_output.hh @@ -0,0 +1,41 @@ +// -*- 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_OUTPUT_HH +#define SPOT_BIN_COMMON_OUTPUT_HH + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif + +#include +#include "ltlvisit/tostring.hh" + +enum output_format_t { spot_output, spin_output, utf8_output }; +extern output_format_t output_format; +extern bool full_parenth; + +extern const struct argp output_argp; + +int parse_opt_output(int key, char* arg, struct argp_state* state); +void output_formula(const spot::ltl::formula* f); + +#endif // SPOT_BIN_COMMON_OUTPUT_HH diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index b3dc59c60..7bb75ed0d 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -80,8 +80,9 @@ #include "error.h" #include -#include "misc/_config.h" +#include "common_output.hh" +#include "misc/_config.h" #include #include #include @@ -90,7 +91,6 @@ #include #include #include "ltlast/allnodes.hh" -#include "ltlvisit/tostring.hh" #include "ltlenv/defaultenv.hh" using namespace spot; @@ -121,8 +121,6 @@ Translation. LNCS 2102\n\ [rv] K. Rozier and M. Vardi (Spin'07): LTL Satisfiability Checking. \ LNCS 4595.\n"; -#define OPT_SPOT 1 - #define OPT_AND_F 2 #define OPT_AND_FG 3 #define OPT_AND_GF 4 @@ -192,14 +190,8 @@ static const argp_option options[] = { "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 }, OPT_ALIAS(gh-u2), OPT_ALIAS(go-phi), - /**************************************************/ - { 0, 0, 0, 0, "Output options:", 6 }, - { "full-parentheses", 'p', 0, 0, - "output fully-parenthesized formulas", 0 }, - { "spin", 's', 0, 0, "output in Spin's syntax", 0 }, - { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", 0 }, - { "utf8", '8', 0, 0, "output using UTF-8 characters", 0 }, /**************************************************/ + { 0, 0, 0, 0, "Output options:", -20 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; @@ -214,9 +206,12 @@ struct job typedef std::vector jobs_t; static jobs_t jobs; -enum output_format_t { spot_output, spin_output, utf8_output }; -static output_format_t output_format = spot_output; -static bool full_parenth = false; + +const struct argp_child children[] = + { + { &output_argp, 0, 0, -20 }, + { 0, 0, 0, 0 } + }; // static int // to_int(const char* s) @@ -275,21 +270,11 @@ enqueue_job(int pattern, const char* range) } static int -parse_opt(int key, char* arg, struct argp_state* state) +parse_opt(int key, char* arg, struct argp_state*) { - (void) state; // This switch is alphabetically-ordered. switch (key) { - case '8': - output_format = utf8_output; - break; - case 'p': - full_parenth = true; - break; - case 's': - output_format = spin_output; - break; case OPT_AND_F: case OPT_AND_FG: case OPT_AND_GF: @@ -310,9 +295,6 @@ parse_opt(int key, char* arg, struct argp_state* state) case OPT_RV_COUNTER_LINEAR: enqueue_job(key, arg); break; - case OPT_SPOT: - output_format = spot_output; - break; default: return ARGP_ERR_UNKNOWN; } @@ -888,19 +870,7 @@ output_pattern(int pattern, int n) error(100, 0, "internal error: pattern not implemented"); } - switch (output_format) - { - case spot_output: - spot::ltl::to_string(f, std::cout, full_parenth); - break; - case spin_output: - spot::ltl::to_spin_string(f, std::cout, full_parenth); - break; - case utf8_output: - spot::ltl::to_utf8_string(f, std::cout, full_parenth); - break; - } - std::cout << "\n"; + output_formula(f); f->destroy(); } @@ -931,7 +901,8 @@ main(int argc, char** argv) // and display help text. argv[0] = const_cast(program_name); - const argp ap = { options, parse_opt, 0, argp_program_doc, 0, 0, 0 }; + const argp ap = { options, parse_opt, 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 86a535b80..9aeea802a 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -32,10 +32,11 @@ #include "progname.h" #include "error.h" +#include "common_output.hh" + #include "misc/_config.h" #include "misc/hash.hh" #include "ltlparse/public.hh" -#include "ltlvisit/tostring.hh" #include "ltlvisit/simplify.hh" #include "ltlvisit/length.hh" #include "ltlast/unop.hh" @@ -61,7 +62,6 @@ Exit status:\n\ 1 if no formula were output (no match)\n\ 2 if any error has been reported"; -#define OPT_SPOT 1 #define OPT_SKIP_ERRORS 2 #define OPT_DROP_ERRORS 3 #define OPT_NNF 4 @@ -154,20 +154,21 @@ static const argp_option options[] = "match formulas implying FORMULA", 0 }, { "equivalent-to", OPT_EQUIVALENT_TO, "FORMULA", 0, "match formulas equivalent to FORMULA", 0 }, - { "invert-match", 'v', 0, 0, "Select non-matching formulas", 0}, - /**************************************************/ - { 0, 0, 0, 0, "Output options:", 6 }, - { "full-parentheses", 'p', 0, 0, - "output fully-parenthesized formulas", 0 }, - { "spin", 's', 0, 0, "output in Spin's syntax", 0 }, - { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", 0 }, - { "utf8", '8', 0, 0, "output using UTF-8 characters", 0 }, - { "unique", 'u', 0, 0, "drop formulas that have already been outpout", 0 }, + { "invert-match", 'v', 0, 0, "select non-matching formulas", 0}, + { "unique", 'u', 0, 0, + "drop formulas that have already been output (not affected by -v)", 0 }, /**************************************************/ + { 0, 0, 0, 0, "Output options:", -20 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, { 0, 0, 0, 0, 0, 0 } }; +const struct argp_child children[] = + { + { &output_argp, 0, 0, -20 }, + { 0, 0, 0, 0 } + }; + struct job { const char* str; @@ -187,9 +188,6 @@ static bool one_match = false; enum error_style_t { drop_errors, skip_errors }; static error_style_t error_style = drop_errors; static bool quiet = false; -enum output_format_t { spot_output, spin_output, utf8_output }; -static output_format_t output_format = spot_output; -static bool full_parenth = false; static bool nnf = false; static bool negate = false; static int level = 0; @@ -242,15 +240,11 @@ parse_formula_arg(const std::string& input) static int -parse_opt(int key, char* arg, struct argp_state* state) +parse_opt(int key, char* arg, struct argp_state*) { - (void) state; // This switch is alphabetically-ordered. switch (key) { - case '8': - output_format = utf8_output; - break; case 'f': jobs.push_back(job(arg, false)); break; @@ -260,9 +254,6 @@ parse_opt(int key, char* arg, struct argp_state* state) case 'n': negate = true; break; - case 'p': - full_parenth = true; - break; case 'q': quiet = true; break; @@ -287,9 +278,6 @@ parse_opt(int key, char* arg, struct argp_state* state) error(2, 0, "invalid simplification level '%s'", arg); } break; - case 's': - output_format = spin_output; - break; case 'u': unique = true; break; @@ -342,9 +330,6 @@ parse_opt(int key, char* arg, struct argp_state* state) case OPT_SKIP_ERRORS: error_style = skip_errors; break; - case OPT_SPOT: - output_format = spot_output; - break; case OPT_SYNTACTIC_SAFETY: syntactic_safety = true; break; @@ -516,19 +501,7 @@ namespace if (matched) { one_match = true; - switch (output_format) - { - case spot_output: - spot::ltl::to_string(f, std::cout, full_parenth); - break; - case spin_output: - spot::ltl::to_spin_string(f, std::cout, full_parenth); - break; - case utf8_output: - spot::ltl::to_utf8_string(f, std::cout, full_parenth); - break; - } - std::cout << "\n"; + output_formula(f); } f->destroy(); @@ -610,7 +583,7 @@ main(int argc, char** argv) argv[0] = const_cast(program_name); const argp ap = { options, parse_opt, "[FILENAME...]", - 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);