diff --git a/NEWS b/NEWS index a193ea39d..03283857b 100644 --- a/NEWS +++ b/NEWS @@ -173,6 +173,10 @@ New in spot 2.9.5.dev (not yet released) - tgba_determinize() could create parity automata using more colors than necessary. + - When passed an incomplete automaton as input, tgba_determinize() + would sometimes produce a complete automaton but incorrectly mark + it as incomplete. + New in spot 2.9.5 (2020-11-19) Bugs fixed: diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index 436b8303a..c3a981353 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -933,9 +933,12 @@ namespace spot { false, // state based false, // inherently_weak false, false, // deterministic - true, // complete + false, // complete true // stutter inv }); + // completeness can only be improved. + if (aut->prop_complete().is_true()) + res->prop_complete(true); // Given a safra_state get its associated state in output automata. // Required to create new edges from 2 safra-state diff --git a/tests/python/298.py b/tests/python/298.py index 51f9f35a1..d4865c440 100644 --- a/tests/python/298.py +++ b/tests/python/298.py @@ -25,9 +25,16 @@ a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""") a1 = spot.degeneralize_tba(a1) r1 = spot.tgba_determinize(a1, True, False, False) assert r1.num_sets() == 3 +assert a1.prop_complete().is_false(); +# This used to fail in 2.9.5 and earlier. +assert r1.prop_complete().is_maybe(); +assert spot.is_complete(r1) a2 = spot.automaton("""genltl --dac=51 | ltl2tgba --high |""") a2 = spot.degeneralize_tba(a2) r2 = spot.tgba_determinize(a2, True, False, False) # This used to fail in 2.9.5 and earlier. assert r2.num_sets() == 3 +assert a2.prop_complete().is_false(); +assert r2.prop_complete().is_maybe(); +assert spot.is_complete(r2)