From a117fe1a22d1735995a9f032c6372611b96e5abc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 7 Feb 2023 14:40:20 +0100
Subject: [PATCH] to_finit: fix issue #526

* spot/twaalgos/remprop.cc: Use bdd_restrict instead of bdd_exists.
* tests/core/ltlf.test: Add test case.
* NEWS: Mention the bug.
---
 NEWS                     |  4 ++++
 spot/twaalgos/remprop.cc |  6 ++---
 tests/core/ltlf.test     | 51 +++++++++++++++++++++++++++++++++++++++-
 3 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index e8774df45..2ffc85d38 100644
--- a/NEWS
+++ b/NEWS
@@ -36,6 +36,10 @@ New in spot 2.11.3.dev  (not yet released)
     done in Spot so far) may require the output to use transition-based
     acceptance.  (Issue #525.)
 
+  - to_finite(), introduce in 2.11, had a bug that could break the
+    completeness of automata and trigger an exception from the HOA
+    printer.  (Issue #526.)
+
 New in spot 2.11.3  (2022-12-09)
 
   Bug fixes:
diff --git a/spot/twaalgos/remprop.cc b/spot/twaalgos/remprop.cc
index 942a1b4b5..8d4be8fbc 100644
--- a/spot/twaalgos/remprop.cc
+++ b/spot/twaalgos/remprop.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2019, 2022 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2015-2019, 2022, 2023 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -205,7 +205,7 @@ namespace spot
             }
           else
             {
-              e.cond = bdd_exist(e.cond, rem);
+              e.cond = bdd_restrict(e.cond, rem);
             }
       }
 
diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test
index 11f2132ac..74a2da79e 100755
--- a/tests/core/ltlf.test
+++ b/tests/core/ltlf.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2022 Laboratoire de Recherche et Développement de
+# Copyright (C) 2022, 2023 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -173,3 +173,52 @@ grep -v '\[f\]' out4 > out3
 cmp out3 out4 && exit 1 # make sure we did remove something
 autfilt out3 > out4
 diff out4 expected3
+
+# Issue #526
+ltlfilt -f '(i->XXo)|G(i<->Xo2)' --from-ltlf | ltl2tgba -D |\
+    autfilt -C --to-finite > out
+cat >exp <<EOF
+HOA: v1
+States: 9
+Start: 0
+AP: 3 "o" "o2" "i"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0 {0}
+[2] 6
+[!2] 7
+State: 1
+[!1&!2] 1
+[!1&2] 5
+[1] 8
+State: 2 {0}
+[0] 7
+[!0] 8
+State: 3 {0}
+[!0&!1&!2] 1
+[!0&!1&2] 5
+[0] 7
+[!0&1] 8
+State: 4 {0}
+[!0&1&!2] 1
+[!0&1&2] 5
+[0] 7
+[!0&!1] 8
+State: 5 {0}
+[1&!2] 1
+[1&2] 5
+[!1] 8
+State: 6 {0}
+[!1] 2
+[1&!2] 3
+[1&2] 4
+State: 7 {0}
+[t] 7
+State: 8
+[t] 8
+--END--
+EOF
+diff out exp