diff --git a/NEWS b/NEWS index b51db0cf1..1f2303187 100644 --- a/NEWS +++ b/NEWS @@ -298,6 +298,11 @@ New in spot 2.9.8.dev (not yet released) - tgba_determinize() could create parity automata using more colors than necessary. (Related to issue #298) + - There were two corners cases under which sat_minimize() would + return the original transition-based automaton when asked to + produce state-based output without changing the acceptance + condition. + Deprecation notices: - twa_graph::defrag_states() and digraph::defrag_states() now take diff --git a/spot/twaalgos/dtbasat.hh b/spot/twaalgos/dtbasat.hh index a2a480566..79f096a1f 100644 --- a/spot/twaalgos/dtbasat.hh +++ b/spot/twaalgos/dtbasat.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2021 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -38,7 +38,7 @@ namespace spot /// turning the TBA into a BA. /// /// If no equivalent deterministic TBA with \a target_state_number - /// states is found, a null pointer + /// states is found, this returns a null pointer. SPOT_API twa_graph_ptr dtba_sat_synthetize(const const_twa_graph_ptr& a, int target_state_number, diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index e3c625ba4..670a9ffc8 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1472,16 +1472,22 @@ namespace spot // returned in the case of a WDBA. complete_here(a); + bool orig_is_valid = false; + if (states == -1 && max_states == -1) { if (state_based) max_states = sbacc(a)->num_states(); else max_states = a->num_states(); - // If we have not user-supplied acceptance, the input - // automaton is a valid one, so we start the search with one - // less state. - max_states -= !user_supplied_acc; + // If we have no user-supplied acceptance, and we are not + // guessing state-based upperbound, the input automaton is a + // valid one, so we start the search with one less state. + if (!user_supplied_acc && (!state_based || a->prop_state_acc())) + { + --max_states; + orig_is_valid = true; + } } @@ -1525,7 +1531,7 @@ namespace spot (a, state_based, sat_langmap, max_states); } - if (!a && !user_supplied_acc) + if (!a && orig_is_valid) a = orig; } else diff --git a/tests/python/satmin.ipynb b/tests/python/satmin.ipynb index 4cec11ad3..ff14b3195 100644 --- a/tests/python/satmin.ipynb +++ b/tests/python/satmin.ipynb @@ -1925,7 +1925,7 @@ "source": [ "How did the procedure look for a complete automaton of size 5 when the input had only 2 states? It's because the input uses transition-based acceptance: to estimate an upper bound of the size of the state-based output, the `sat_minimize()` procedure converted its transition-based input to state-based acceptance (using the `spot.sbacc()` function) and counted the number of states in the result.\n", "\n", - "Such an estimate is not necessarily correct of we request a different acceptance condition. In that case We can actually change the upper-bound using `max_states`. Below we additionally demonstrate the use of the `colored` option, to request all transition to belong to exactly one set, as customary in parity automata." + "Such an estimate is not necessarily correct if we request a different acceptance condition. In that case we can actually change the upper-bound using `max_states`. Below we additionally demonstrate the use of the `colored` option, to request all transitions to belong to exactly one set, as customary in parity automata." ] }, { @@ -4253,7 +4253,7 @@ "source": [ "### `states`\n", "\n", - "Sometimes we do not want a minimization loop, we just want to generate an equivalent automaton with a given number of states. In that case, we use the `states` option. However there is no constraint that all state should be reachable, so in the end, you could end with an automaton with fewer states than requested." + "Sometimes we do not want a minimization loop, we just want to generate an equivalent automaton with a given number of states. In that case, we use the `states` option. However there is no constraint that all states should be reachable, so in the end, you could end with an automaton with fewer states than requested." ] }, { @@ -4588,7 +4588,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.9.1+" + "version": "3.9.2" } }, "nbformat": 4, diff --git a/tests/python/satmin.py b/tests/python/satmin.py index 156b27ea8..2d28dd405 100644 --- a/tests/python/satmin.py +++ b/tests/python/satmin.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2020 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2020, 2021 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -237,3 +237,13 @@ min4 = spot.sat_minimize(aut, acc='parity max odd 3', colored=True, sat_naive=True) assert min4.num_sets() == 3 assert min4.num_states() == 2 + + +aut = spot.translate('GFa') +assert aut.num_sets() == 1 +assert aut.num_states() == 1 +assert aut.is_deterministic() +out = spot.sat_minimize(aut, state_based=True) +assert out.num_states() == 2 +out = spot.sat_minimize(aut, state_based=True, max_states=1) +assert out is None