diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 1142220d7..3da54a67e 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -208,6 +208,8 @@ namespace spot twa_graph_ptr postprocessor::finalize(twa_graph_ptr tmp) const { + if (PREF_ != Any && level_ != Low) + tmp->remove_unused_ap(); if (COMP_) tmp = complete(tmp); bool want_parity = type_ & Parity; @@ -364,7 +366,6 @@ namespace spot if (m->num_states() <= a->num_states()) a = m; } - a->remove_unused_ap(); } return finalize(a); } @@ -666,8 +667,6 @@ namespace spot sim = dba ? dba : sim; - sim->remove_unused_ap(); - if (type_ == CoBuchi) { unsigned ns = sim->num_states(); diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index eb838e7b5..4db8643f9 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013-2018, 2020-2021 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -383,17 +383,14 @@ namespace spot || type_ == GeneralizedBuchi) aut2 = gf_guarantee_to_ba_maybe(r, simpl_->get_dict(), det, state_based_); - if (aut2 && (type_ & (Buchi | Parity)) - && (pref_ & Deterministic)) + if (aut2 && (pref_ & Deterministic)) return finalize(aut2); if (!aut2 && (type_ == Generic || type_ & (Parity | CoBuchi))) { aut2 = fg_safety_to_dca_maybe(r, simpl_->get_dict(), state_based_); - if (aut2 - && (type_ & (CoBuchi | Parity)) - && (pref_ & Deterministic)) + if (aut2 && (pref_ & Deterministic)) return finalize(aut2); } } diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index de6a9dc27..7e512c17a 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2021 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -376,8 +376,8 @@ cat >formulas <\n" ], "text/plain": [ - " *' at 0x7fc69c0f16c0> >" + " *' at 0x7fe43cde71b0> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d909240> >" + " *' at 0x7fe43c131fc0> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d9099c0> >" + " *' at 0x7fe43c1563c0> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc69e19d9c0> >" + " *' at 0x7fe43c131ba0> >" ] }, "execution_count": 8, @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d916150> >" + " *' at 0x7fe43c156e40> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d916450> >" + " *' at 0x7fe43c163300> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d916a20> >" + " *' at 0x7fe43c163810> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91ca20> >" + " *' at 0x7fe43c1694b0> >" ] }, "metadata": {}, @@ -1974,7 +1974,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c9c0> >" + " *' at 0x7fe43c163210> >" ] }, "metadata": {}, @@ -2132,7 +2132,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91cd80> >" + " *' at 0x7fe43c169180> >" ] }, "metadata": {}, @@ -2280,7 +2280,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91ccc0> >" + " *' at 0x7fe43c169360> >" ] }, "metadata": {}, @@ -2469,7 +2469,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91cb40> >" + " *' at 0x7fe43c169210> >" ] }, "execution_count": 19, @@ -2545,7 +2545,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d925690> >" + " *' at 0x7fe43c169fc0> >" ] }, "execution_count": 20, @@ -3095,7 +3095,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c480> >" + " *' at 0x7fe43c156ea0> >" ] }, "metadata": {}, @@ -3195,7 +3195,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c510> >" + " *' at 0x7fe43c156210> >" ] }, "execution_count": 24, @@ -3254,21 +3254,21 @@ "0->0\n", "\n", "\n", - "a\n", + "!a\n", + "\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fc68d91c2d0> >" + " *' at 0x7fe440654c60> >" ] }, "execution_count": 25, @@ -3439,7 +3439,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d9164e0> >" + " *' at 0x7fe43c1316c0> >" ] }, "execution_count": 27, @@ -3522,7 +3522,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c480> >" + " *' at 0x7fe43c156ea0> >" ] }, "metadata": {}, @@ -3587,7 +3587,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c480> >" + " *' at 0x7fe43c156ea0> >" ] }, "metadata": {}, @@ -3674,7 +3674,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc68d91c480> >" + " *' at 0x7fe43c156ea0> >" ] }, "execution_count": 29, @@ -3707,7 +3707,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.6" + "version": "3.9.1+" } }, "nbformat": 4, diff --git a/tests/python/toparity.py b/tests/python/toparity.py index a7b034f21..eebadfdd3 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -1,6 +1,6 @@ #!/usr/bin/python3 # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -112,7 +112,7 @@ def test(aut, expected_num_states=[], full=True): spot.reduce_parity_here(p1) assert spot.are_equivalent(aut, p1) if expected_num is not None: - # print(p1.num_states(), expected_num) + print(p1.num_states(), expected_num) assert p1.num_states() == expected_num if full: # Make sure passing opt is the same as setting @@ -391,4 +391,4 @@ for f in spot.randltl(5, 2000): a = spot.translate('!(GFa -> (GFb & GF(!b & !Xb)))', 'gen', 'det') b = spot.to_parity_old(a, True) assert a.equivalent_to(b) -test(a, [7, 7, 3, 7, 8, 7, 3]) +test(a, [7, 7, 3, 7, 7, 7, 3])