From d9045d131c5c1bfa16f25af4bf1dd62a972a2839 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 24 Jan 2015 22:55:57 +0100 Subject: [PATCH] bin: factor common conversion functions * src/bin/common_conv.cc, src/bin/common_conv.hh: New files. * src/bin/Makefile.am: Add them. * src/bin/autfilt.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc: Use them. --- src/bin/Makefile.am | 4 ++- src/bin/autfilt.cc | 37 +++---------------- src/bin/common_conv.cc | 82 ++++++++++++++++++++++++++++++++++++++++++ src/bin/common_conv.hh | 36 +++++++++++++++++++ src/bin/ltlcross.cc | 41 +-------------------- src/bin/ltlfilt.cc | 20 +---------- src/bin/ltlgrind.cc | 30 ++++------------ src/bin/randaut.cc | 21 +---------- src/bin/randltl.cc | 13 ++----- 9 files changed, 136 insertions(+), 148 deletions(-) create mode 100644 src/bin/common_conv.cc create mode 100644 src/bin/common_conv.hh diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 4410d71ea..07c1230c5 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -28,6 +28,8 @@ noinst_LIBRARIES = libcommon.a libcommon_a_SOURCES = \ common_aoutput.cc \ common_aoutput.hh \ + common_conv.hh \ + common_conv.cc \ common_cout.hh \ common_cout.cc \ common_finput.cc \ diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 9b408b59a..9dcd33ce4 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -34,6 +34,7 @@ #include "common_aoutput.hh" #include "common_range.hh" #include "common_post.hh" +#include "common_conv.hh" #include "tgbaalgos/product.hh" #include "tgbaalgos/isdet.hh" @@ -169,36 +170,6 @@ static char opt_instut = 0; static bool opt_is_empty = false; static std::unique_ptr opt_uniq = nullptr; -static int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); - return res; -} - -static int -to_pos_int(const char* s) -{ - int res = to_int(s); - if (res < 0) - error(2, 0, "%d is not positive", res); - return res; -} - -static spot::tgba_digraph_ptr -read_automaton(const char* filename) -{ - spot::hoa_parse_error_list pel; - auto p = hoa_parse(filename, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, filename, pel) - || !p || p->aborted) - error(2, 0, "failed to read automaton from %s", filename); - return std::move(p->aut); -} - static int parse_opt(int key, char* arg, struct argp_state*) { @@ -238,7 +209,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_ARE_ISOMORPHIC: - opt_are_isomorphic = read_automaton(arg); + opt_are_isomorphic = read_automaton(arg, dict); break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); @@ -252,7 +223,7 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "unknown argument for --instut: %s", arg); break; case OPT_INTERSECT: - opt_intersect = read_automaton(arg); + opt_intersect = read_automaton(arg, dict); break; case OPT_DESTUT: opt_destut = true; @@ -271,7 +242,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_PRODUCT: { - auto a = read_automaton(arg); + auto a = read_automaton(arg, dict); if (!opt_product) opt_product = std::move(a); else diff --git a/src/bin/common_conv.cc b/src/bin/common_conv.cc new file mode 100644 index 000000000..707a6abbf --- /dev/null +++ b/src/bin/common_conv.cc @@ -0,0 +1,82 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 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 3 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 this program. If not, see . + +#include "common_conv.hh" +#include +#include "error.h" +#include "hoaparse/public.hh" + +int +to_int(const char* s) +{ + char* endptr; + int res = strtol(s, &endptr, 10); + if (*endptr) + error(2, 0, "failed to parse '%s' as an integer.", s); + return res; +} + +int +to_pos_int(const char* s) +{ + int res = to_int(s); + if (res < 0) + error(2, 0, "%d is not positive", res); + return res; +} + +unsigned +to_unsigned (const char *s) +{ + char* endptr; + unsigned res = strtoul(s, &endptr, 10); + if (*endptr) + error(2, 0, "failed to parse '%s' as an unsigned integer.", s); + return res; +} + +float +to_float(const char* s) +{ + char* endptr; + float res = strtof(s, &endptr); + if (*endptr) + error(2, 0, "failed to parse '%s' as a float.", s); + return res; +} + +float +to_probability(const char* s) +{ + float res = to_float(s); + if (res < 0.0 || res > 1.0) + error(2, 0, "%f is not between 0 and 1.", res); + return res; +} + +spot::tgba_digraph_ptr +read_automaton(const char* filename, spot::bdd_dict_ptr& dict) +{ + spot::hoa_parse_error_list pel; + auto p = spot::hoa_parse(filename, pel, dict); + if (spot::format_hoa_parse_errors(std::cerr, filename, pel) + || !p || p->aborted) + error(2, 0, "failed to read automaton from %s", filename); + return std::move(p->aut); +} diff --git a/src/bin/common_conv.hh b/src/bin/common_conv.hh new file mode 100644 index 000000000..0d6cedda7 --- /dev/null +++ b/src/bin/common_conv.hh @@ -0,0 +1,36 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 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 3 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 this program. If not, see . + +#ifndef SPOT_BIN_COMMON_CONV_HH +#define SPOT_BIN_COMMON_CONV_HH + +#include "common_sys.hh" +#include "tgba/tgbagraph.hh" + +int to_int(const char* s); +int to_pos_int(const char* s); +unsigned to_unsigned (const char *s); +float to_float(const char* s); +float to_probability(const char* s); + +spot::tgba_digraph_ptr +read_automaton(const char* filename, spot::bdd_dict_ptr& dict); + + +#endif // SPOT_BIN_COMMON_CONV_HH diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 3850acd74..ab3831cc3 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -35,6 +35,7 @@ #include "common_setup.hh" #include "common_cout.hh" +#include "common_conv.hh" #include "common_finput.hh" #include "dstarparse/public.hh" #include "hoaparse/public.hh" @@ -466,46 +467,6 @@ typedef std::vector statistics_vector; statistics_vector vstats; std::vector formulas; -static int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); - return res; -} - -static int -to_pos_int(const char* s) -{ - int res = to_int(s); - if (res < 0) - error(2, 0, "%d is not positive", res); - return res; -} - -static float -to_float(const char* s) -{ - char* endptr; - // Do not use strtof(), it does not exist on Solaris 9. - float res = strtod(s, &endptr); - if (*endptr) - error(2, 0, "failed to parse '%s' as a float.", s); - return res; -} - -static float -to_probability(const char* s) -{ - float res = to_float(s); - if (res < 0.0 || res > 1.0) - error(2, 0, "%f is not between 0 and 1.", res); - return res; -} - - static int parse_opt(int key, char* arg, struct argp_state*) { diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index f66339214..80dcb2fd2 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -31,6 +31,7 @@ #include "common_finput.hh" #include "common_output.hh" #include "common_cout.hh" +#include "common_conv.hh" #include "common_r.hh" #include "misc/hash.hh" @@ -239,25 +240,6 @@ static const spot::ltl::formula* implied_by = 0; static const spot::ltl::formula* imply = 0; static const spot::ltl::formula* equivalent_to = 0; -static int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); - return res; -} - -static int -to_pos_int(const char* s) -{ - int res = to_int(s); - if (res < 0) - error(2, 0, "%d is not positive", res); - return res; -} - static const spot::ltl::formula* parse_formula_arg(const std::string& input) { diff --git a/src/bin/ltlgrind.cc b/src/bin/ltlgrind.cc index 942681d79..6da8e373b 100644 --- a/src/bin/ltlgrind.cc +++ b/src/bin/ltlgrind.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -20,10 +20,13 @@ #include "common_sys.hh" #include +#include "error.h" + #include "common_setup.hh" #include "common_finput.hh" #include "common_output.hh" -#include "error.h" +#include "common_conv.hh" + #include "ltlast/allnodes.hh" #include "ltlvisit/clone.hh" #include "ltlvisit/apcollect.hh" @@ -89,30 +92,9 @@ static const argp_child children[] = { {0, 0, 0, 0} }; -static int -to_int(const char *s) -{ - char* endptr; - unsigned res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an unsigned integer.", s); - return res; -} - -static unsigned -to_unsigned (const char *s) -{ - char* endptr; - unsigned res = strtoul(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an unsigned integer.", s); - return res; -} - namespace { - class mutate_processor: - public job_processor + class mutate_processor: public job_processor { public: int diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index e8824a2a4..0b08cfee5 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -31,6 +31,7 @@ #include "common_range.hh" #include "common_cout.hh" #include "common_aoutput.hh" +#include "common_conv.hh" #include "ltlenv/defaultenv.hh" #include "misc/timer.hh" @@ -115,26 +116,6 @@ static bool opt_state_acc = false; static bool ba_wanted = false; static std::unique_ptr opt_uniq = nullptr; -static int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); - return res; -} - -static float -to_float(const char* s) -{ - char* endptr; - float res = strtof(s, &endptr); - if (*endptr) - error(2, 0, "failed to parse '%s' as a float.", s); - return res; -} - static void ba_options() { diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 0c1e0e502..7f111a7c4 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,6 +30,7 @@ #include "common_output.hh" #include "common_range.hh" #include "common_r.hh" +#include "common_conv.hh" #include #include "ltlast/multop.hh" @@ -179,16 +180,6 @@ GF_n(spot::ltl::atomic_prop_set& ap) return res; } -static int -to_int(const char* s) -{ - char* endptr; - int res = strtol(s, &endptr, 10); - if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); - return res; -} - static int parse_opt(int key, char* arg, struct argp_state* as) {