From e22a800fe4af26826b6a7b9bcc83656d0a35f191 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Feb 2015 23:13:47 +0100 Subject: [PATCH] ltlfilt: add a --count option, like autfilt * src/bin/common_output.cc, src/bin/common_output.hh: Add count_output. * src/bin/ltlfilt.cc: Add the --count option. * src/ltltest/ltlfilt.test: Test it. * NEWS: Mention it. --- NEWS | 3 +++ src/bin/common_output.cc | 7 ++++--- src/bin/common_output.hh | 6 +++--- src/bin/ltlfilt.cc | 27 +++++++++++++++++++++------ src/ltltest/ltlfilt.test | 4 ++++ 5 files changed, 35 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 585362ed4..b914b9b2d 100644 --- a/NEWS +++ b/NEWS @@ -41,6 +41,9 @@ New in spot 1.99a (not yet released) now. The short '-n NUM' option is now the same as the new --max-count=N option, for consistency with other tools. + - ltlfilt has a new --count option to count the number of matching + automata. + - ltlcross (and ltldo) have a list of hard-coded shorthands for some existing tools. So for instance running 'ltlcross spin ...' is the same as running diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 1cf5f926a..1d039d97e 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.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. @@ -104,6 +104,7 @@ stream_formula(std::ostream& out, case latex_output: spot::ltl::to_latex_string(f, out, full_parenth); break; + case count_output: case quiet_output: break; } @@ -261,10 +262,10 @@ output_formula_checked(const spot::ltl::formula* f, const char* filename, int linenum, const char* prefix, const char* suffix) { - if (output_format == quiet_output) + if (output_format == quiet_output || output_format == count_output) return; output_formula(std::cout, f, filename, linenum, prefix, suffix); - std::cout << std::endl; + std::cout << '\n'; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). check_cout(); diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index 781d04b36..5492c56c6 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// 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. // @@ -29,7 +29,7 @@ enum output_format_t { spot_output, spin_output, utf8_output, lbt_output, wring_output, latex_output, - quiet_output }; + quiet_output, count_output }; extern output_format_t output_format; extern bool full_parenth; extern bool escape_csv; diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 80dcb2fd2..87e94021a 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -168,6 +168,7 @@ static const argp_option options[] = "drop formulas that have already been output (not affected by -v)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, + { "count", 'c', 0, 0, "print only a count of matched formulas", 0 }, { "quiet", 'q', 0, 0, "suppress all normal output", 0 }, { "max-count", 'n', "NUM", 0, "output at most NUM formulas", 0 }, { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\ @@ -235,6 +236,7 @@ static bool stutter_insensitive = false; static bool ap = false; static unsigned ap_n = 0; static int opt_max_count = -1; +static long int match_count = 0; static const spot::ltl::formula* implied_by = 0; static const spot::ltl::formula* imply = 0; @@ -258,6 +260,9 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { + case 'c': + output_format = count_output; + break; case 'n': opt_max_count = to_pos_int(arg); break; @@ -472,7 +477,7 @@ namespace process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { - if (opt_max_count == 0) + if (opt_max_count >= 0 && match_count >= opt_max_count) { abort_run = true; f->destroy(); @@ -607,8 +612,7 @@ namespace { one_match = true; output_formula_checked(f, filename, linenum, prefix, suffix); - if (opt_max_count > 0) - --opt_max_count; + ++match_count; } f->destroy(); return 0; @@ -635,8 +639,19 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier_options opt = simplifier_options(); opt.boolean_to_isop = boolean_to_isop; spot::ltl::ltl_simplifier simpl(opt); - ltl_processor processor(simpl); - if (processor.run()) - return 2; + try + { + ltl_processor processor(simpl); + if (processor.run()) + return 2; + } + catch (const std::runtime_error& e) + { + error(2, 0, "%s", e.what()); + } + + if (output_format == count_output) + std::cout << match_count << std::endl; + return one_match ? 0 : 1; } diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index 6af667b97..03616b843 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -83,6 +83,10 @@ F(a & !Xa & Xb) a & (b | c) EOF +checkopt -c --stutter-invariant <