From a1c02856acfd5421f16c8fa22c182f3766b75e76 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 24 Jan 2023 11:35:14 +0100
Subject: [PATCH] autfilt: allow --highlight-word to work on Fin acceptance

Fixes #523.

* bin/autfilt.cc: Remove the restriction.
* tests/core/acc_word.test: Add test case.
* NEWS: Mention the fix.
---
 NEWS                     |  4 ++++
 bin/autfilt.cc           |  9 ++-------
 tests/core/acc_word.test | 20 +++++++++++++-------
 3 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/NEWS b/NEWS
index e6d484f12..10ecce97c 100644
--- a/NEWS
+++ b/NEWS
@@ -10,6 +10,10 @@ New in spot 2.11.3.dev  (not yet released)
     multiple initial states (because Spot supports only one), the HOA
     parser could break state-based acceptance.  (Issue #522.)
 
+  - autfilt --highlight-word refused to work on automata with Fin
+    acceptance for historical reasons, however the code has been
+    perfectly able to handle this for a while.  (Issue #523.)
+
   - delay_branching_here(), a new optimization of Spot 2.11 had an
     incorrect handling of states without successors, causing some
     segfaults.  (Issue #524.)
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index b55d1bc9f..4487fad8b 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1667,13 +1667,8 @@ namespace
 
       if (!opt->hl_words.empty())
         for (auto& [word_aut, color]: opt->hl_words)
-          {
-            if (aut->acc().uses_fin_acceptance())
-              error(2, 0,
-                    "--highlight-word does not yet work with Fin acceptance");
-            if (auto run = spot::product(aut, word_aut)->accepting_run())
-              run->project(aut)->highlight(color);
-          }
+          if (auto run = spot::product(aut, word_aut)->accepting_run())
+            run->project(aut)->highlight(color);
 
       timer.stop();
       if (opt->uniq)
diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test
index 53ce4b98e..5f3b6880b 100644
--- a/tests/core/acc_word.test
+++ b/tests/core/acc_word.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2016, 2017, 2018, 2019 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2016-2019, 2023 Laboratoire de Recherche
+# et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -91,6 +91,15 @@ State: 1
 EOF
 diff expected out
 
+ltl2tgba -G '(GF(a & X!a) -> GF(b & XXb)) & GFc' > aut.hoa
+word='!a&!c;cycle{!a&b&!c;!a&c;!a&b&c}'
+autfilt -H1.1 aut.hoa --highlight-word="$word" > out.hoa
+grep spot.highlight.edges out.hoa >out.edges
+cat >expected <<EOF
+spot.highlight.edges: 3 1 11 1 12 1
+EOF
+diff out.edges expected
+
 ltl2tgba 'Fa & Fb' |
     autfilt -H1.1 \
             --highlight-word='2,!a&!b;cycle{!a&b;a&b}' \
@@ -133,11 +142,8 @@ for w in ',!a&!b;cycle{!a&b;a&b}' '-1,cycle{a}' '1 cycle{a}'; do
 done
 
 
-# highlight-word does not yet work with Fin acceptance
-ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}' 2>stderr && exit 1
-test $? -eq 2
-grep 'highlight-word.*Fin' stderr
-
+# highlight-word used not to work with Fin acceptance, but it's ok now
+ltl2tgba -G -D 'FGa' | autfilt --highlight-word='cycle{a}'
 
 ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1
 ltlfilt -f 'GF!a' --accept-word 'cycle{!a}'