From 8fd594f5d0b3ef815e4be6ad690c33996b0e3bb0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 14 Jan 2015 18:49:00 +0100 Subject: [PATCH] ltlfilt: add a --max-count/-n option This fixes #44. * src/bin/ltlfilt.cc: Implement -n/--max-count. * doc/org/ltlfilt.org, src/tgbatest/randpsl.test: Use it * NEWS: Document it. --- NEWS | 4 ++++ doc/org/ltlfilt.org | 49 +++++++++++++++++++-------------------- src/bin/ltlfilt.cc | 22 ++++++++++++++++++ src/tgbatest/randpsl.test | 4 +++- 4 files changed, 53 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index 6121f32d7..654eb11d2 100644 --- a/NEWS +++ b/NEWS @@ -29,6 +29,10 @@ New in spot 1.99a (not yet released) same as in grep (and also autfilt): disable all normal input, for situtations where only the exit status matters. + - ltlfilt's old -n/--negate option can only be used as --negate + now. The short '-n NUM' option is now the same as the new + --max-count=N option, for consistency with other tools. + - There is a parser for the HOA format (http://adl.github.io/hoaf/) available as a spot::hoa_stream_parser object or spot::hoa_parse() function. diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 2b8448732..20cab6b7e 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -234,30 +234,29 @@ formulas that respect certain constraints. For instance let us generate 10 formulas that are equivalent to =a U b=: #+BEGIN_SRC sh :results verbatim :exports both -randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' | head -n 10 +randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' -n 10 #+END_SRC #+RESULTS: #+begin_example -!(!a R !b) -(!Gb -> a) U b a U b -Fb & (a W b) -((a <-> !(a | b)) W a) U ((!b M b) U b) -(b <-> (Xb M a)) -> b +(b W Fb) & ((Fb xor (a W b)) -> (a U b)) +(b U (a W b)) U b +!(!b W (!a & !b)) +(a M (a <-> (a xor !a))) U b +(a U b) | ((a & Xa) M Gb) (a | b) U b -((!b U b) -> (a W b)) U b -(a xor b) U b -b R (Fb & (a U (a W b))) +(b xor !b) -> ((b W a) U b) +(!a -> ((a W b) W (a & b))) U b +(a U b) | (Ga U b) #+end_example The =-n -1= option to =randltl= will cause it to output an infinite stream of random formulas. =ltlfilt=, which reads its standard input by default, will select only those equivalent to =a U b=. The output -of =ltlfilt= would still be an infinite stream of random formulas, so -we display only the first 10 using the standard =head= utility. Less -trivial formulas could be obtained by adding the =-r= option to -=randltl= (or equivalently adding the =-r= and =-u= option to -=ltlfilt=). +of =ltlfilt= is limited to 10 formulas using =-n 10=. (As would using +=| head -n 10=.) Less trivial formulas could be obtained by adding +the =-r= option to =randltl= (or equivalently adding the =-r= and =-u= +option to =ltlfilt=). Another similar example, that requires two calls to =ltlfilt=, is the @@ -268,20 +267,20 @@ then ignoring all syntactic safety formulas, and keeping only the safety formulas in the remaining list. #+BEGIN_SRC sh :results verbatim :exports both -randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety | head -n 10 +randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety -n 10 #+END_SRC #+RESULTS: #+begin_example -(!a & Fa) R Xa -!a | (a & b) | (((!a & b) | (a & !b)) M (!a M X!a)) -G(!a M Xa) -G((G!b & !a) | (a & Fb)) R a -G!a M !a -G(!a M ((!b & XGb) | (b & XF!b))) -F(b | G!b) -F(Xa | G!a) -G(XXa | (b & F!a)) -G((!a & (!a M !b)) | (a & (a W b))) +G(!b | Gb | X(b & Fa)) +((!a | X(!a R (!b U !a))) & X((!a & !b) | (a & b))) | (a & X(((!a & b) | (a & !b)) & (b R a))) +(F!a & (a | G!a)) R Xa +(b M XGb) W XXa +G(Xa & (!a U G!b)) +(a & F!a) R X(a | b) +!a | (a & (a M !b)) +b U XGb +(!a | (a R (!a | Xa))) M X!a +Ga | (!b U !a) #+end_example diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 910c0098f..286619583 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -166,6 +166,7 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, { "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 "\ "the following interpreted sequences:", -19 }, { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, @@ -230,6 +231,7 @@ static bool remove_x = false; static bool stutter_insensitive = false; static bool ap = false; static unsigned ap_n = 0; +static int opt_max_count = -1; static const spot::ltl::formula* implied_by = 0; static const spot::ltl::formula* imply = 0; @@ -245,6 +247,14 @@ to_int(const char* 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) @@ -264,6 +274,9 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { + case 'n': + opt_max_count = to_pos_int(arg); + break; case 'q': output_format = quiet_output; break; @@ -475,6 +488,13 @@ namespace process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { + if (opt_max_count == 0) + { + abort_run = true; + f->destroy(); + return 0; + } + if (negate) f = spot::ltl::unop::instance(spot::ltl::unop::Not, f); @@ -603,6 +623,8 @@ namespace { one_match = true; output_formula_checked(f, filename, linenum, prefix, suffix); + if (opt_max_count > 0) + --opt_max_count; } f->destroy(); return 0; diff --git a/src/tgbatest/randpsl.test b/src/tgbatest/randpsl.test index 41821a635..c8e183b60 100755 --- a/src/tgbatest/randpsl.test +++ b/src/tgbatest/randpsl.test @@ -27,6 +27,8 @@ set -e # formulae, and that have a size of at lease 12. ../../bin/randltl -n -1 --tree-size 30 --seed 0 --psl a b c | ../../bin/ltlfilt -r --size-min 12 --unique | -../../bin/ltlfilt -v --ltl | head -n 50 | +../../bin/ltlfilt -v --ltl -n 50 | tee formulas | ../../bin/ltlcross '../ltl2tgba -R3 -t %f >%T' '../ltl2tgba -x -R3 -t %f >%T' \ -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}' + +test `wc -l < formulas` = 50