From f7b5dcf47da2fa77a8ae6ff28fc67377233f2051 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 12 Feb 2016 19:53:52 +0100 Subject: [PATCH] autfilt: add support for --are-equivalent Fixes #17. * bin/autfilt.cc: Implement it. * tests/core/included.test: Test it. * NEWS: Mention it. --- NEWS | 3 +++ bin/autfilt.cc | 17 +++++++++++++++++ tests/core/included.test | 25 +++++++++++++++++++++++++ 3 files changed, 45 insertions(+) diff --git a/NEWS b/NEWS index 1ce61f79a..52e43df6e 100644 --- a/NEWS +++ b/NEWS @@ -40,6 +40,9 @@ New in spot 1.99.7a (not yet released) * autfilt has a new option, --included-in, to filter automata whose language are included in the language of a given automaton. + * autfilt has a new option, --equivalent-to, to filter automata + that are equivalent (language-wise) to a given automaton. + Library: * Building products with different dictionaries now raise an diff --git a/bin/autfilt.cc b/bin/autfilt.cc index fc3b162f2..af81f5fd8 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -79,6 +79,7 @@ enum { OPT_DESTUT, OPT_DNF_ACC, OPT_EDGES, + OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, OPT_GENERIC, OPT_INSTUT, @@ -210,6 +211,9 @@ static const argp_option options[] = { "included-in", OPT_INCLUDED_IN, "FILENAME", 0, "keep automata whose languages are included in that of the " "automaton from FILENAME", 0 }, + { "equivalent-to", OPT_EQUIVALENT_TO, "FILENAME", 0, + "keep automata thare are equivalent (language-wise) to the automaton " + "in FILENAME", 0 }, { "invert-match", 'v', nullptr, 0, "select non-matching automata", 0 }, { "states", OPT_STATES, "RANGE", 0, "keep automata whose number of states are in RANGE", 0 }, @@ -264,6 +268,8 @@ static struct opt_t spot::twa_graph_ptr product_or = nullptr; spot::twa_graph_ptr intersect = nullptr; spot::twa_graph_ptr included_in = nullptr; + spot::twa_graph_ptr equivalent_pos = nullptr; + spot::twa_graph_ptr equivalent_neg = nullptr; spot::twa_graph_ptr are_isomorphic = nullptr; std::unique_ptr isomorphism_checker = nullptr; @@ -380,6 +386,13 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_EXCLUSIVE_AP: opt->excl_ap.add_group(arg); break; + case OPT_EQUIVALENT_TO: + if (opt->equivalent_pos) + error(2, 0, "only one --equivalent-to option can be given"); + opt->equivalent_pos = read_automaton(arg, opt->dict); + opt->equivalent_neg = + spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos)); + break; case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) opt_instut = 1; @@ -627,6 +640,10 @@ namespace matched &= !spot::product(aut, opt->intersect)->is_empty(); if (opt->included_in) matched &= spot::product(aut, opt->included_in)->is_empty(); + if (opt->equivalent_pos) + matched &= spot::product(aut, opt->equivalent_neg)->is_empty() + && spot::product(dtwa_complement(ensure_deterministic(aut)), + opt->equivalent_pos)->is_empty(); // Drop or keep matched automata depending on the --invert option if (matched == opt_invert) diff --git a/tests/core/included.test b/tests/core/included.test index 114ee0609..9f39fef20 100755 --- a/tests/core/included.test +++ b/tests/core/included.test @@ -37,3 +37,28 @@ run 1 autfilt -q gfa.hoa --included-in fga.hoa run 0 autfilt -q gab.hoa --included-in fga.hoa --included-in fgb.hoa run 1 autfilt -q ga.hoa --included-in fga.hoa --included-in fgb.hoa run 0 autfilt -q false.hoa --included-in fga.hoa + +run 1 autfilt -q gfa.hoa --equivalent-to fga.hoa +run 1 autfilt -q fga.hoa --equivalent-to gfa.hoa + +run 0 autfilt -D fga.hoa > fgaD.hoa +grep deterministic fga.hoa && exit 1 +grep deterministic fgaD.hoa +run 0 autfilt -q fga.hoa --equivalent-to fgaD.hoa +run 0 autfilt -q fgaD.hoa --equivalent-to fga.hoa + + +# lets test that +# (a U b) + !(a U b) == true + +ltl2tgba 'a U b' > a1.hoa +ltl2tgba '!(a U b)' | autfilt --product-or a1.hoa > out.hoa +ltl2tgba true | autfilt out.hoa --equivalent-to - + + +# This should fails if we replace !(a U b) by !(a U c). +ltl2tgba '!(a U c)' | autfilt --product-or a1.hoa > out.hoa +ltl2tgba true | autfilt out.hoa --equivalent-to - && exit 1 + +: +