diff --git a/NEWS b/NEWS index c734fb995..0886eb41d 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,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 <