From e2ec711c4037a7e930ff30195715e05995e919dc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 11 Mar 2020 23:05:15 +0100
Subject: [PATCH] autfilt: fix -u

Fixes #399.

* bin/autfilt.cc: Fix it.
* tests/core/isomorph.test: Add test case.
* NEWS: Mention the issue.
---
 NEWS                     |  3 +++
 bin/autfilt.cc           | 33 +++++++++++++++++++++++++++------
 tests/core/isomorph.test |  8 +++++++-
 3 files changed, 37 insertions(+), 7 deletions(-)

diff --git a/NEWS b/NEWS
index f4a991052..c5e90b8ca 100644
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,9 @@ New in spot 2.8.6.dev (not yet released)
     incorrectly tagged as complete, causing the print_hoa() function
     to raise an exception.
 
+  - autfilt --uniq was not considering differences in acceptance
+    conditions or number of states when discarding automata.
+
 New in spot 2.8.6 (2020-02-19)
 
   Bugs fixed:
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index e0f8279b2..00b16b83d 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -419,8 +419,31 @@ static const struct argp_child children[] =
   };
 
 
-typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
-typedef std::set<std::vector<tr_t>> unique_aut_t;
+struct canon_aut
+{
+  typedef spot::twa_graph::graph_t::edge_storage_t tr_t;
+  unsigned num_states;
+  std::vector<tr_t> edges;
+  std::string acc;
+
+  canon_aut(const spot::const_twa_graph_ptr& aut)
+    : num_states(aut->num_states())
+    , edges(aut->edge_vector().begin() + 1,
+            aut->edge_vector().end())
+  {
+    std::ostringstream os;
+    aut->get_acceptance().to_text(os);
+    acc = os.str();
+  }
+
+  bool operator<(const canon_aut& o) const
+  {
+    return std::tie(num_states, edges, acc)
+      < std::tie(o.num_states, o.edges, o.acc);
+  };
+};
+
+typedef std::set<canon_aut> unique_aut_t;
 static long int match_count = 0;
 static spot::option_map extra_options;
 static bool randomize_st = false;
@@ -703,8 +726,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       opt_max_count = to_pos_int(arg, "-n/--max-count");
       break;
     case 'u':
-      opt->uniq =
-        std::unique_ptr<unique_aut_t>(new std::set<std::vector<tr_t>>());
+      opt->uniq = std::unique_ptr<unique_aut_t>(new std::set<canon_aut>());
       break;
     case 'v':
       opt_invert = true;
@@ -1559,8 +1581,7 @@ namespace
           auto tmp =
             spot::canonicalize(make_twa_graph(aut,
                                                  spot::twa::prop_set::all()));
-          if (!opt->uniq->emplace(tmp->edge_vector().begin() + 1,
-                                  tmp->edge_vector().end()).second)
+          if (!opt->uniq->emplace(tmp).second)
             return 0;
         }
 
diff --git a/tests/core/isomorph.test b/tests/core/isomorph.test
index 37c3e43d3..a331f7399 100755
--- a/tests/core/isomorph.test
+++ b/tests/core/isomorph.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
+# Copyright (C) 2014, 2015, 2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -109,3 +109,9 @@ run 0 autfilt aut3 --are-isomorphic aut4
 
 run 0 autfilt -u aut1 aut2 aut2 aut3 -c >out
 test 2 = "`cat out`"
+
+ltl2tgba -D -G GFa > aut1
+ltl2tgba -D -G FGa > aut2
+test 0 = `autfilt -c --are-isomorphic aut1 aut2`
+test 2 = `ltl2tgba -D -G 'GFa' 'FG!a' | autfilt -u -c`
+test 1 = `ltl2tgba -D -G 'GFa' 'GFa' | autfilt -u -c`