autfilt: add support for --are-equivalent

Fixes #17.

* bin/autfilt.cc: Implement it.
* tests/core/included.test: Test it.
* NEWS: Mention it.

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

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<spot::isomorphism_checker>
                          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)

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
+
+:
+