From 7e2e4df1bbe0b87e63207b7bf8be8df390bb5d33 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Mar 2016 11:10:59 +0100 Subject: [PATCH] autfilt: add a --reject-word option * bin/autfilt.cc: Implement --reject-word. * NEWS, doc/org/autfilt.org: More doc. * tests/core/acc_word.test: More tests. --- NEWS | 9 ++++++--- bin/autfilt.cc | 35 +++++++++++++++++++++++++++++++---- doc/org/autfilt.org | 36 ++++++++++++++++++++++++++++++++++++ tests/core/acc_word.test | 31 ++++++++++++++++++++++++++++++- 4 files changed, 103 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index cd093861a..08f5c0480 100644 --- a/NEWS +++ b/NEWS @@ -2,12 +2,15 @@ New in spot 1.99.8a (not yet released) Command-line tools: - * autfilt has a new option: --accept-word=WORD, that filters automata - that accept WORD. This option can be used several times, and will - filter automata that accept all words. + * autfilt has two new options: --accept-word=WORD and + --reject-word=WORD for filtering automata that accept or reject + some word. The option may be used multiple times. Library: + * The parse_word() function can be used to parse a lasso-shaped + word and build a twa_word. The twa_word::as_automaton() + method can be used to create an automaton out of that. * twa::ap_var() renamed to twa::ap_vars(). * emptiness_check_instantiator::min_acceptance_conditions() and emptiness_check_instantiator::max_acceptance_conditions() renamed diff --git a/bin/autfilt.cc b/bin/autfilt.cc index d90c9af97..6be6d401a 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -70,7 +70,7 @@ Exit status:\n\ // Keep this list sorted enum { OPT_ACC_SETS = 256, - OPT_ACC_WORD, + OPT_ACCEPT_WORD, OPT_AP_N, OPT_ARE_ISOMORPHIC, OPT_CLEAN_ACC, @@ -101,6 +101,7 @@ enum { OPT_PRODUCT_AND, OPT_PRODUCT_OR, OPT_RANDOMIZE, + OPT_REJECT_WORD, OPT_REM_AP, OPT_REM_DEAD, OPT_REM_UNREACH, @@ -226,9 +227,15 @@ static const argp_option options[] = "keep automata whose number of edges are in RANGE", 0 }, { "acc-sets", OPT_ACC_SETS, "RANGE", 0, "keep automata whose number of acceptance sets are in RANGE", 0 }, - { "accept-word", OPT_ACC_WORD, "WORD", 0, - "keep automata that recognize WORD", 0 }, + { "accept-word", OPT_ACCEPT_WORD, "WORD", 0, + "keep automata that accept WORD", 0 }, + { "reject-word", OPT_REJECT_WORD, "WORD", 0, + "keep automata that reject WORD", 0 }, RANGE_DOC_FULL, + { nullptr, 0, nullptr, 0, + "WORD is lasso-shaped and written as 'BF;BF;...;BF;cycle{BF;...;BF}' " + "where BF are arbitrary Boolean formulas. The 'cycle{...}' part is " + "mandatory, but the prefix can be omitted.", 0 }, { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " "then the simplification level defaults to --high unless specified " @@ -284,6 +291,7 @@ static struct opt_t spot::exclusive_ap excl_ap; spot::remove_ap rem_ap; std::vector acc_words; + std::vector rej_words; }* opt; static bool opt_merge = false; @@ -366,7 +374,7 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ACC_SETS: opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; - case OPT_ACC_WORD: + case OPT_ACCEPT_WORD: try { opt->acc_words.push_back(spot::parse_word(arg, opt->dict) @@ -537,6 +545,18 @@ parse_opt(int key, char* arg, struct argp_state*) randomize_st = true; } break; + case OPT_REJECT_WORD: + try + { + opt->rej_words.push_back(spot::parse_word(arg, opt->dict) + ->as_automaton()); + } + catch (const spot::parse_error& e) + { + error(2, 0, "failed to parse the argument of --reject-word:\n%s", + e.what()); + } + break; case OPT_REM_AP: opt->rem_ap.add_ap(arg); break; @@ -677,6 +697,13 @@ namespace matched = false; break; } + if (matched && !opt->rej_words.empty()) + for (auto& word_aut: opt->rej_words) + if (!spot::product(aut, word_aut)->is_empty()) + { + matched = false; + break; + } // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 2755b539d..468e75cb5 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -163,9 +163,16 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d' #+begin_example --acc-sets=RANGE keep automata whose number of acceptance sets are in RANGE + --accept-word=WORD keep automata that accept WORD + --ap=RANGE match automata with a number of atomic + propositions in RANGE --are-isomorphic=FILENAME keep automata that are isomorphic to the automaton in FILENAME --edges=RANGE keep automata whose number of edges are in RANGE + --equivalent-to=FILENAME keep automata thare are equivalent + (language-wise) to the automaton in FILENAME + --included-in=FILENAME keep automata whose languages are included in that + of the automaton from FILENAME --intersect=FILENAME keep automata whose languages have an non-empty intersection with the automaton from FILENAME --is-complete keep complete automata @@ -175,6 +182,7 @@ autfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d' --is-terminal keep only terminal automata --is-unambiguous keep only unambiguous automata --is-weak keep only weak automata + --reject-word=WORD keep automata that reject WORD --states=RANGE keep automata whose number of states are in RANGE -u, --unique do not output the same automaton twice (same in the sense that they are isomorphic) @@ -716,3 +724,31 @@ rm -f example.hoa aut-ex1.hoa ltl2tgba 'a U b U c' | autfilt --accept-word 'b; cycle{c}' -q && echo "word accepted" #+END_SRC + + +Here is an example where we generate an infinite stream of random LTL +formulas using [[file:randltl.org][=randltl=]], convert them all to automata using +[[file:ltl2tgba.org][=ltl2tgba=]], filter out the first 10 automata that accept both the +words =a&!b;cycle{!a&!b}= and =!a&!b;cycle{a&b}= yet reject any word +of the form =cycle{b}=, and display the associated formula (which was +stored as the name of the automaton by =ltl2tgba=). + +#+BEGIN_SRC sh :results verbatim :export both +randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- | + autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ + --reject-word='cycle{b}' --stats=%M -n 10 +#+END_SRC + +#+RESULTS: +#+begin_example +F!b +!b +F(!a & !b) +(!a & (XX!a | (!a W F!b))) R !b +F(Fb R !b) +Fa R F!b +Fa U !b +!b & X(!b W Ga) +Fb R F!b +XF!b U (!b & (!a | G!b)) +#+end_example diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 87c759faf..1a0ca1fff 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -18,6 +18,7 @@ # You should have received a copy of the GNU General Public License # along with this program. If not, see . +. ./defs # The --accept-word option filters automata that accept the given word # If several words are given, it filters automata that accept ALL words @@ -29,4 +30,32 @@ ltl2tgba -f 'a U b' | autfilt --accept-word='cycle{!a}' --accept-word='a;cycle{b}' -q ltl2tgba -f 'a U b' | autfilt --accept-word='cycle{!b}' -q && exit 1 -: + +# An example from the documentation: +randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- | + autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ + --reject-word='cycle{b}' --stats=%M -n 3 > out +cat >expect <error && exit 1 +autfilt --accept='cycle{foo' >error && exit 1 +cat error +cat >expect <>> foobar + ^ +A twa_word must contain a cycle + +autfilt: failed to parse the argument of --accept-word: +>>> cycle{foo + ^ +Missing ';' or '}' after formula + +EOF +diff expect error