From f759697e1c22fc0e316751927ced7fea183cb418 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 1 Feb 2022 16:35:41 +0100
Subject: [PATCH] autfilt: add --aliases=drop|keep option

* bin/autfilt.cc: Here.
* spot/twaalgos/hoa.cc, spot/twaalgos/hoa.hh: Fix the prototype
of set_aliases so that it is usable.
* tests/core/dualize.test: Add a simple test case.
* NEWS: Mention the new option.
---
 NEWS                    |  6 ++++++
 bin/autfilt.cc          | 33 ++++++++++++++++++++++++++++-
 spot/twaalgos/hoa.cc    |  2 +-
 spot/twaalgos/hoa.hh    |  2 +-
 tests/core/dualize.test | 47 +++++++++++++++++++++++++++++++++++++++--
 5 files changed, 85 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 2db5d63c9..1dcf7f564 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,11 @@
 New in spot 2.10.4.dev  (net yet released)
 
+  Command-line tools:
+
+  - autfilt has a new options --aliases=drop|keep to specify
+    if the output code should attempt to preserve aliases
+    present in the HOA input.  This defaults to "keep".
+
   Library:
 
   - "original-classes" is a new named property similar to
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index cef86c26c..8f72a96c5 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -88,6 +88,7 @@ enum {
   OPT_ACC_SETS,
   OPT_ACCEPT_WORD,
   OPT_ACCEPTANCE_IS,
+  OPT_ALIASES,
   OPT_AP_N,
   OPT_ARE_ISOMORPHIC,
   OPT_CLEAN_ACC,
@@ -175,6 +176,10 @@ static const argp_option options[] =
     /**************************************************/
     { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 },
     { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 },
+    { "aliases", OPT_ALIASES, "drop|keep", 0,
+      "If the input automaton uses HOA aliases, this decides whether their "
+      "preservation should be attempted in the output.  The default is "
+      "\"keep\".", 3 },
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Filtering options:", 5 },
     { "ap", OPT_AP_N, "RANGE", 0,
@@ -474,6 +479,20 @@ static gra_type const gra_types[] =
 };
 ARGMATCH_VERIFY(gra_args, gra_types);
 
+static bool opt_aliases = true;
+static char const* const aliases_args[] =
+{
+  "drop", "no", "false", "0",
+  "keep", "yes", "true", "1",
+  nullptr,
+};
+static bool const aliases_types[] =
+{
+  false, false, false, false,
+  true, true, true, true,
+};
+ARGMATCH_VERIFY(aliases_args, aliases_types);
+
 enum acc_type {
   ACC_Any = 0,
   ACC_Given,
@@ -757,6 +776,9 @@ parse_opt(int key, char* arg, struct argp_state*)
           error(2, 0, "failed to parse --options near '%s'", opt);
       }
       break;
+    case OPT_ALIASES:
+      opt_aliases = XARGMATCH("--aliases", arg, aliases_args, aliases_types);
+      break;
     case OPT_AP_N:
       opt_ap_n = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
@@ -1363,6 +1385,8 @@ namespace
       spot::process_timer timer;
       timer.start();
 
+      auto aliases = get_aliases(haut->aut);
+
       // If --stats or --name is used, duplicate the automaton so we
       // never modify the original automaton (e.g. with
       // merge_edges()) and the statistics about it make sense.
@@ -1660,6 +1684,13 @@ namespace
 
       ++match_count;
 
+      if (aliases)
+        {
+          if (opt_aliases)
+            set_aliases(aut, *aliases);
+          else
+            set_aliases(aut, {});
+        }
       printer.print(aut, timer, nullptr, haut->filename.c_str(), -1,
                     haut, prefix, suffix);
 
diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index 1d3b9fbac..20cd93173 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -970,7 +970,7 @@ namespace spot
   }
 
   void
-  set_aliases(twa_ptr& g, std::vector<std::pair<std::string, bdd>> aliases)
+  set_aliases(twa_ptr g, std::vector<std::pair<std::string, bdd>> aliases)
   {
     if (aliases.empty())
       {
diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh
index 59effb419..22b2170e4 100644
--- a/spot/twaalgos/hoa.hh
+++ b/spot/twaalgos/hoa.hh
@@ -61,5 +61,5 @@ namespace spot
   ///
   /// Pass an empty vector to remove existing aliases.
   SPOT_API void
-  set_aliases(twa_ptr& g, std::vector<std::pair<std::string, bdd>> aliases);
+  set_aliases(twa_ptr g, std::vector<std::pair<std::string, bdd>> aliases);
 }
diff --git a/tests/core/dualize.test b/tests/core/dualize.test
index 53bbec8fc..da5a65747 100755
--- a/tests/core/dualize.test
+++ b/tests/core/dualize.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2019, 2021 Laboratoire de Recherche et
+# Copyright (C) 2017, 2019, 2021, 2022 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -72,6 +72,10 @@ HOA: v1
 States: 10
 Start: 0&4
 AP: 2 "p0" "p1"
+Alias: @a 0&!1
+Alias: @b !0&!1
+Alias: @c 0&1
+Alias: @d !0&1
 Acceptance: 2 Inf(0) | Inf(1)
 properties: trans-labels explicit-labels trans-acc univ-branch
 --BODY--
@@ -104,7 +108,8 @@ State: 9
 [!0] 9
 --END--
 EOF
-autfilt --dualize <input2 >output2
+autfilt --dualize --aliases=drop <input2 >output2
+autfilt --dualize <input2 >>output2
 cat >expected2<<EOF
 HOA: v1
 States: 9
@@ -140,5 +145,43 @@ State: 8
 [!1] 0&6&7
 [!0&!1] 0&7
 --END--
+HOA: v1
+States: 9
+Start: 8
+AP: 2 "p0" "p1"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels state-acc univ-branch
+Alias: @a 0&!1
+Alias: @b !0&!1
+Alias: @c 0&1
+Alias: @d !@c&!@b&!@a
+--BODY--
+State: 0
+[@a] 0&6&7
+[@b] 0&7
+State: 1
+[@c | @a] 1&2&3
+[@d | @b] 1&3
+State: 2
+[@c | @a] 4
+State: 3
+[@c | @a] 4
+[@d | @b] 5
+State: 4
+[t] 4
+State: 5
+[@d | @b] 5
+State: 6 {0}
+[@d | @b] 4
+[@c | @a] 6
+State: 7
+[@b | @a] 7
+State: 8
+[t] 1&2&3
+[@d | @b] 1&3
+[@b | @a] 0&6&7
+[@b] 0&7
+--END--
 EOF
 diff output2 expected2