diff --git a/NEWS b/NEWS index d31ba4dff..b4f51a0d8 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,11 @@ New in spot 2.8.5.dev (not yet released) - Nothing yet. + Bugs fixed: + + - degeneralize_tba() was incorrectly not honnoring the "skip_level" + optimization after creating an accepting transition; as a + consequence, some correct output could be larger than necessary + (but still correct). New in spot 2.8.5 (2020-01-04) diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 397ec33da..cbbd372bc 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -580,7 +580,7 @@ namespace spot { d.second = 0; // Make it go to the first level. // Skip as many levels as possible. - if (!a->acc().accepting(acc) && !skip_levels) + if (!a->acc().accepting(acc) && skip_levels) { if (use_cust_acc_orders) { diff --git a/tests/python/simstate.py b/tests/python/simstate.py index e2bf5330e..8e5e1c712 100644 --- a/tests/python/simstate.py +++ b/tests/python/simstate.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018, 2020 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -169,7 +169,9 @@ State: 11 "{₀[1#1]{₁[0#0,0#1]{₂[1#0]₂}₁}₀}" a = spot.translate('!Gp0 xor FG((p0 W Gp1) M p1)') a = spot.degeneralize_tba(a) +assert a.num_states() == 8 b = spot.simulation(a) +assert b.num_states() == 3 b.set_init_state(1) b.purge_unreachable_states() b.copy_state_names_from(a) @@ -182,7 +184,7 @@ Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- -State: 0 "[1,8,9]" +State: 0 "[1,7]" [!1] 0 {0} [1] 0 --END--"""