diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index a5004bf91..ee1c873b2 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -28,8 +28,8 @@ LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a bin_PROGRAMS = ltlfilt genltl randltl -noinst_HEADERS = common_output.hh common_range.hh +noinst_HEADERS = common_output.hh common_range.hh common_r.hh -ltlfilt_SOURCES = ltlfilt.cc common_output.cc +ltlfilt_SOURCES = ltlfilt.cc common_output.cc common_r.cc genltl_SOURCES = genltl.cc common_output.cc common_range.cc -randltl_SOURCES = randltl.cc common_output.cc common_range.cc +randltl_SOURCES = randltl.cc common_output.cc common_range.cc common_r.cc diff --git a/src/bin/common_r.cc b/src/bin/common_r.cc new file mode 100644 index 000000000..9a6b78ff2 --- /dev/null +++ b/src/bin/common_r.cc @@ -0,0 +1,69 @@ +// -*- 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. + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif + +#include "error.h" + +#include "common_r.hh" + +int simplification_level = 0; + +void +parse_r(const char* arg) +{ + if (!arg) + { + simplification_level = 3; + return; + } + if (arg[1] == 0 && arg[0] >= '0' && arg[0] <= '3') + { + simplification_level = arg[0] - '0'; + return; + } + error(2, 0, "invalid simplification level '%s'", arg); +} + +spot::ltl::ltl_simplifier_options +simplifier_options() +{ + spot::ltl::ltl_simplifier_options options; + switch (simplification_level) + { + case 3: + options.containment_checks = true; + options.containment_checks_stronger = true; + // fall through + case 2: + options.synt_impl = true; + // fall through + case 1: + options.reduce_basics = true; + options.event_univ = true; + // fall through + default: + break; + } + return options; +} diff --git a/src/bin/common_r.hh b/src/bin/common_r.hh new file mode 100644 index 000000000..045b51daa --- /dev/null +++ b/src/bin/common_r.hh @@ -0,0 +1,50 @@ +// -*- 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_R_HH +#define SPOT_BIN_COMMON_R_HH + +#include "ltlvisit/simplify.hh" + +#define OPT_R 'r' + +#define DECLARE_OPT_R \ + { "simplify", OPT_R, "LEVEL", OPTION_ARG_OPTIONAL, \ + "simplify formulas according to LEVEL (see below); LEVEL is " \ + "set to 3 if omitted", 0 } + +#define LEVEL_DOC(g) \ + { 0, 0, 0, 0, "The simplification LEVEL may be set as follows.", g }, \ + { " 0", 0, 0, OPTION_DOC | OPTION_NO_USAGE, \ + "No rewriting", 0 }, \ + { " 1", 0, 0, OPTION_DOC | OPTION_NO_USAGE, \ + "basic rewritings and eventual/universal rules", 0 }, \ + { " 2", 0, 0, OPTION_DOC | OPTION_NO_USAGE, \ + "additional syntactic implication rules", 0 }, \ + { " 3", 0, 0, OPTION_DOC | OPTION_NO_USAGE, \ + "better implications using containment", 0 } + +extern int simplification_level; + +void parse_r(const char* arg); +spot::ltl::ltl_simplifier_options simplifier_options(); + +#endif // SPOT_BIN_COMMON_RANGE_HH diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 9aeea802a..742c36b7e 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -33,6 +33,7 @@ #include "error.h" #include "common_output.hh" +#include "common_r.hh" #include "misc/_config.h" #include "misc/hash.hh" @@ -104,17 +105,8 @@ static const argp_option options[] = { 0, 0, 0, 0, "Transformation options:", 3 }, { "negate", 'n', 0, 0, "negate each formula", 0 }, { "nnf", OPT_NNF, 0, 0, "rewrite formulas in negative normal form", 0 }, - { "simplify", 'r', "LEVEL", OPTION_ARG_OPTIONAL, - "simplify formulas according to LEVEL (see below)", 0 }, - { 0, 0, 0, 0, " The simplification LEVEL might be one of:", 4 }, - { " 0", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "No rewriting", 0 }, - { " 1", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "basic rewritings and eventual/universal rules", 0 }, - { " 2", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "additional syntactic implication rules", 0 }, - { " 3", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "better implications using containment (default)", 0 }, + DECLARE_OPT_R, + LEVEL_DOC(4), /**************************************************/ { 0, 0, 0, 0, "Filtering options (matching is done after transformation):", 5 }, @@ -190,7 +182,6 @@ static error_style_t error_style = drop_errors; static bool quiet = false; static bool nnf = false; static bool negate = false; -static int level = 0; static bool unique = false; static bool psl = false; static bool ltl = false; @@ -257,26 +248,8 @@ parse_opt(int key, char* arg, struct argp_state*) case 'q': quiet = true; break; - case 'r': - if (!arg) - { - level = 3; - break; - } - else - { - if (arg[1] == 0) - switch (arg[0]) - { - case '0': - case '1': - case '2': - case '3': - level = arg[0] = '0'; - return 0; - } - error(2, 0, "invalid simplification level '%s'", arg); - } + case OPT_R: + parse_r(arg); break; case 'u': unique = true; @@ -419,7 +392,7 @@ namespace if (negate) f = spot::ltl::unop::instance(spot::ltl::unop::Not, f); - if (level) + if (simplification_level) { const spot::ltl::formula* res = simpl.simplify(f); f->destroy(); @@ -538,26 +511,7 @@ namespace static int run_jobs() { - spot::ltl::ltl_simplifier_options options; - - switch (level) - { - case 3: - options.containment_checks = true; - options.containment_checks_stronger = true; - // fall through - case 2: - options.synt_impl = true; - // fall through - case 1: - options.reduce_basics = true; - options.event_univ = true; - // fall through - default: - break; - } - - spot::ltl::ltl_simplifier simpl(options); + spot::ltl::ltl_simplifier simpl(simplifier_options()); ltl_processor processor(simpl); int error = 0; diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index 6395ff968..53f3bb88a 100644 --- a/src/bin/randltl.cc +++ b/src/bin/randltl.cc @@ -32,6 +32,7 @@ #include "common_output.hh" #include "common_range.hh" +#include "common_r.hh" #include "misc/_config.h" #include @@ -95,9 +96,11 @@ static const argp_option options[] = "tree size of the formulas generated, before mandatory "\ "trivial simplifications (15)", 0 }, { "unique", 'u', 0, 0, "do not generate duplicate formulas", 0 }, + DECLARE_OPT_R, RANGE_DOC, + LEVEL_DOC(3), /**************************************************/ - { 0, 0, 0, 0, "Adjusting probabilities:", 3 }, + { 0, 0, 0, 0, "Adjusting probabilities:", 4 }, { "dump-priorities", OPT_DUMP_PRIORITIES, 0, 0, "show current priorities, do not generate any formula", 0 }, { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0, @@ -162,6 +165,9 @@ parse_opt(int key, char* arg, struct argp_state*) case 'P': output = OutputPSL; break; + case OPT_R: + parse_r(arg); + break; case 'S': output = OutputSERE; break; @@ -304,6 +310,8 @@ main(int argc, char** argv) fset_t unique_set; + spot::ltl::ltl_simplifier simpl(simplifier_options()); + while (opt_formulas < 0 || opt_formulas--) { #define MAX_TRIALS 100000 @@ -318,6 +326,12 @@ main(int argc, char** argv) if (size != opt_tree_size.max) size = spot::rrand(size, opt_tree_size.max); f = rf->generate(size); + if (simplification_level) + { + const spot::ltl::formula* tmp = simpl.simplify(f); + f->destroy(); + f = tmp; + } if (opt_unique) { if (unique_set.insert(f).second)