From 59e1f6a3396f56faf9afd936bc68862a4e3c7cd1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 9 Apr 2016 10:10:41 +0200 Subject: [PATCH] ltlfilt: implement --reject-word and --accept-word * bin/common_range.hh: Store the common definition of words. * bin/autfilt.cc: Use it. * bin/ltlfilt.cc: Likewise, and implement those two options. * tests/core/acc_word.test: Test them. * doc/org/autfilt.org: Augment the last example to point out that it can now be done with ltlfilt. * NEWS: Mention the new options. --- NEWS | 6 ++- bin/autfilt.cc | 5 +-- bin/common_range.hh | 20 ++++++--- bin/ltlfilt.cc | 96 ++++++++++++++++++++++++++++++++-------- doc/org/autfilt.org | 22 +++++++++ tests/core/acc_word.test | 6 +++ 6 files changed, 124 insertions(+), 31 deletions(-) diff --git a/NEWS b/NEWS index 8a90f1d50..53e2e3bd1 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 1.99.9a (not yet released) - Nothing yet. + Command-line tools: + + * ltlfilt now also support the --accept-word=WORD and + --reject-word=WORD options that were introduced in autfilt in the + previous version. New in spot 1.99.9 (2016-03-14) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e0155a4e7..5a001ba11 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -232,10 +232,7 @@ static const argp_option options[] = { "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 }, + WORD_DOC, { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " "then the simplification level defaults to --high unless specified " diff --git a/bin/common_range.hh b/bin/common_range.hh index 0fae93aa6..2727ef934 100644 --- a/bin/common_range.hh +++ b/bin/common_range.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -19,17 +19,23 @@ #pragma once -#define RANGE_DOC \ - { nullptr, 0, nullptr, 0, \ - "RANGE may have one of the following forms: 'INT', " \ +#define RANGE_DOC \ + { nullptr, 0, nullptr, 0, \ + "RANGE may have one of the following forms: 'INT', " \ "'INT..INT', or '..INT'.\nIn the latter case, the missing number " \ "is assumed to be 1.", 0 } -#define RANGE_DOC_FULL \ - { nullptr, 0, nullptr, 0, \ - "RANGE may have one of the following forms: 'INT', " \ +#define RANGE_DOC_FULL \ + { nullptr, 0, nullptr, 0, \ + "RANGE may have one of the following forms: 'INT', " \ "'INT..INT', '..INT', or 'INT..'", 0 } +#define WORD_DOC \ + { 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 } + struct range { int min; diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index cd727abf5..dd3c1c35f 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -48,6 +48,8 @@ #include #include #include +#include +#include const char argp_program_doc[] ="\ Read a list of formulas and output them back after some optional processing.\v\ @@ -57,7 +59,8 @@ Exit status:\n\ 2 if any error has been reported"; enum { - OPT_AP_N = 256, + OPT_ACCEPT_WORD = 256, + OPT_AP_N, OPT_BOOLEAN, OPT_BOOLEAN_TO_ISOP, OPT_BSIZE, @@ -76,6 +79,7 @@ enum { OPT_NEGATE, OPT_NNF, OPT_OBLIGATION, + OPT_REJECT_WORD, OPT_RELABEL, OPT_RELABEL_BOOL, OPT_REMOVE_WM, @@ -199,7 +203,12 @@ static const argp_option options[] = { "invert-match", 'v', nullptr, 0, "select non-matching formulas", 0}, { "unique", 'u', nullptr, 0, "drop formulas that have already been output (not affected by -v)", 0 }, + { "accept-word", OPT_ACCEPT_WORD, "WORD", 0, + "keep formulas that accept WORD", 0 }, + { "reject-word", OPT_REJECT_WORD, "WORD", 0, + "keep formulas that reject WORD", 0 }, RANGE_DOC_FULL, + WORD_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", -20 }, { "count", 'c', nullptr, 0, "print only a count of matched formulas", 0 }, @@ -275,11 +284,14 @@ static long int match_count = 0; // accessing deleted stuff. static struct opt_t { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::exclusive_ap excl_ap; std::unique_ptr output_define = nullptr; spot::formula implied_by = nullptr; spot::formula imply = nullptr; spot::formula equivalent_to = nullptr; + std::vector acc_words; + std::vector rej_words; }* opt; static std::string unabbreviate; @@ -322,6 +334,18 @@ parse_opt(int key, char* arg, struct argp_state*) // FIXME: use stat() to distinguish filename from string? jobs.emplace_back(arg, true); break; + case OPT_ACCEPT_WORD: + try + { + opt->acc_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 --accept-word:\n%s", + e.what()); + } + break; case OPT_BOOLEAN: boolean = true; break; @@ -388,6 +412,18 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_OBLIGATION: obligation = 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_RELABEL: case OPT_RELABEL_BOOL: relabeling = (key == OPT_RELABEL_BOOL ? BseRelabeling : ApRelabeling); @@ -603,24 +639,46 @@ namespace || simpl.are_equivalent(f, opt->equivalent_to); matched &= !stutter_insensitive || spot::is_stutter_invariant(f); - // Match obligations and subclasses using WDBA minimization. - // Because this is costly, we compute it later, so that we don't - // have to compute it on formulas that have been discarded for - // other reasons. - if (matched && obligation) + if (matched && (obligation + || !opt->acc_words.empty() + || !opt->rej_words.empty())) { auto aut = ltl_to_tgba_fm(f, simpl.get_dict()); - auto min = minimize_obligation(aut, f); - assert(min); - if (aut == min) + + if (matched && !opt->acc_words.empty()) + for (auto& word_aut: opt->acc_words) + if (spot::product(aut, word_aut)->is_empty()) + { + 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; + } + + // Match obligations and subclasses using WDBA minimization. + // Because this is costly, we compute it later, so that we don't + // have to compute it on formulas that have been discarded for + // other reasons. + if (matched && obligation) { - // Not an obligation - matched = false; - } - else - { - matched &= !guarantee || is_terminal_automaton(min); - matched &= !safety || is_safety_mwdba(min); + auto min = minimize_obligation(aut, f); + assert(min); + if (aut == min) + { + // Not an obligation + matched = false; + } + else + { + matched &= !guarantee || is_terminal_automaton(min); + matched &= !safety || is_safety_mwdba(min); + } } } @@ -676,9 +734,9 @@ main(int argc, char** argv) if (boolean_to_isop && simplification_level == 0) simplification_level = 1; - spot::tl_simplifier_options opt(simplification_level); - opt.boolean_to_isop = boolean_to_isop; - spot::tl_simplifier simpl(opt); + spot::tl_simplifier_options tlopt(simplification_level); + tlopt.boolean_to_isop = boolean_to_isop; + spot::tl_simplifier simpl(tlopt, opt->dict); ltl_processor processor(simpl); if (processor.run()) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 975b57c6c..65e445dfb 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -756,3 +756,25 @@ Fa U !b Fb R F!b XF!b U (!b & (!a | G!b)) #+end_example + +Note that the above example could be simplified using the +=--accept-word= and =--reject-word= options of =ltlfilt= directly. +However this demonstrates that using =--stats=%M=, it is possible to +filter formulas based on some properties of automata that have been +generated by from them. The translator needs not be =ltl2tgba=: other +tools can be wrapped with [[file:ltldo.org][=ltldo --name=%f=]] to ensure they work well +in a pipeline and preserve the formula name in the HOA output. For +example Here is a list of 5 LTL formulas that =ltl2dstar= converts to +Rabin automata that have exactly 4 states: + +#+BEGIN_SRC sh :results verbatim :exports both +randltl -n -1 a b | ltlfilt --simplify --remove-wm | + ltldo ltl2dstar --name=%f | autfilt --states=4 --stats=%M -n 5 +#+END_SRC + +#+RESULTS: +: Gb | G!b +: b R (a | b) +: (a & !b & (b | (F!a U (!b & F!a)))) | (!a & (b | (!b & (Ga R (b | Ga))))) +: (a & (a U !b)) | (!a & (!a R b)) +: a | G((a & GFa) | (!a & FG!a)) diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 1a0ca1fff..d66e07834 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -42,6 +42,12 @@ F(!a & !b) EOF diff out expect +# The same, without using automata explicitly +randltl -n -1 a b | ltlfilt --simplify --uniq \ + --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ + --reject-word='cycle{b}' -n 3 > out +diff out expect + # Test syntax errors autfilt --reject='foobar' error && exit 1 autfilt --accept='cycle{foo' >error && exit 1