From 947ab17b1234a6990515a7e744b6a4a4cfb9d906 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 23 Jan 2015 22:48:15 +0100 Subject: [PATCH] autfilt: add an --intersect filter * src/bin/autfilt.cc: Add option --intersect. Factor the code to read automata. * src/tgbatest/neverclaimread.test: Rewrite the tests, replacing 3 calls to ltl2tgba by a single call to autfilt. --- src/bin/autfilt.cc | 42 ++++++++++++++++++++------------ src/tgbatest/neverclaimread.test | 27 +++++++++++--------- 2 files changed, 42 insertions(+), 27 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index d1943fad7..9b408b59a 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -70,6 +70,7 @@ Exit status:\n\ #define OPT_DESTUT 13 #define OPT_INSTUT 14 #define OPT_IS_EMPTY 15 +#define OPT_INTERSECT 16 static const argp_option options[] = { @@ -113,6 +114,9 @@ static const argp_option options[] = "the automaton is deterministic", 0 }, { "is-empty", OPT_IS_EMPTY, 0, 0, "keep automata with an empty language", 0 }, + { "intersect", OPT_INTERSECT, "FILENAME", 0, + "keep automata whose languages have an non-empty intersection with" + " the automaton from FILENAME", 0 }, { "invert-match", 'v', 0, 0, "select non-matching automata", 0 }, { "states", OPT_STATES, "RANGE", 0, "keep automata whose number of states are in RANGE", 0 }, @@ -148,6 +152,7 @@ static bool randomize_tr = false; static int opt_seed = 0; static auto dict = spot::make_bdd_dict(); static spot::tgba_digraph_ptr opt_product = nullptr; +static spot::tgba_digraph_ptr opt_intersect = nullptr; static bool opt_merge = false; static std::unique_ptr isomorphism_checker = nullptr; @@ -183,6 +188,17 @@ to_pos_int(const char* s) return res; } +static spot::tgba_digraph_ptr +read_automaton(const char* filename) +{ + spot::hoa_parse_error_list pel; + auto p = hoa_parse(filename, pel, dict); + if (spot::format_hoa_parse_errors(std::cerr, filename, pel) + || !p || p->aborted) + error(2, 0, "failed to read automaton from %s", filename); + return std::move(p->aut); +} + static int parse_opt(int key, char* arg, struct argp_state*) { @@ -222,15 +238,8 @@ parse_opt(int key, char* arg, struct argp_state*) opt_accsets = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_ARE_ISOMORPHIC: - { - spot::hoa_parse_error_list pel; - auto p = hoa_parse(arg, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, arg, pel) - || !p || p->aborted) - error(2, 0, "failed to read automaton from %s", arg); - opt_are_isomorphic = std::move(p->aut); - break; - } + opt_are_isomorphic = read_automaton(arg); + break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -242,6 +251,9 @@ parse_opt(int key, char* arg, struct argp_state*) else error(2, 0, "unknown argument for --instut: %s", arg); break; + case OPT_INTERSECT: + opt_intersect = read_automaton(arg); + break; case OPT_DESTUT: opt_destut = true; break; @@ -259,16 +271,12 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_PRODUCT: { - spot::hoa_parse_error_list pel; - auto p = hoa_parse(arg, pel, dict); - if (spot::format_hoa_parse_errors(std::cerr, arg, pel) - || !p || p->aborted) - error(2, 0, "failed to read automaton from %s", arg); + auto a = read_automaton(arg); if (!opt_product) - opt_product = std::move(p->aut); + opt_product = std::move(a); else opt_product = spot::product(std::move(opt_product), - std::move(p->aut)); + std::move(a)); } break; case OPT_RANDOMIZE: @@ -369,6 +377,8 @@ namespace matched &= isomorphism_checker->is_isomorphic(aut); if (opt_is_empty) matched &= aut->is_empty(); + if (opt_intersect) + matched &= !spot::product(aut, opt_intersect)->is_empty(); // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index bfbd29edf..bbca2c11d 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -369,26 +369,31 @@ GF("(a + b) == 42" U "process@foo") EOF while read f do - run 0 ../ltl2tgba -b -f "!($f)" > f.tgba + run 0 ../../bin/ltl2tgba -H "!($f)" > f.hoa + run 0 ../../bin/ltl2tgba -s -f "$f" > f.spot + # Make sure there is no `!x' occurring in the + # output. Because `x' is usually #define'd, we + # should use `!(x)' in guards. + grep '![^(].*->' f.spot && exit 1 + # In case we cannot run spin or ltl2ba, use the spot output + cp f.spot f.spin + cp f.spot f.ltl2ba + sf=`../../bin/ltlfilt -sf "$f"` + if test -n "$SPIN"; then # Old spin versions cannot parse formulas such as ((a + b) == 42). - if $SPIN -f "$sf" > f.spin; then - run 0 ../ltl2tgba -E -Pf.tgba -XN f.spin - fi + $SPIN -f "$sf" > f.spin.tmp && mv f.spin.tmp f.spin fi case $f in *\"*);; *) if test -n "$LTL2BA"; then $LTL2BA -f "$sf" > f.ltl2ba - run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba fi esac - run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot - # Make sure there is no `!x' occurring in the - # output. Because `x' is usually #define'd, we - # should use `!(x)' in guards. - grep '![^(].*->' f.spot && exit 1 - run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot + + run 0 ../../bin/autfilt --count -v --intersect=f.hoa \ + f.spot f.spin f.ltl2ba >out + test 3 = `cat out` done