determinize: do not copy the "incomplete" property
Mentioned in issue #298. * spot/twaalgos/determinize.cc: Do not copy prop_complete of the input if it is false. * tests/python/298.py: Test it. * NEWS: Mention the bug.
This commit is contained in:
parent
f6be083050
commit
7e2f091839
3 changed files with 15 additions and 1 deletions
4
NEWS
4
NEWS
|
|
@ -173,6 +173,10 @@ New in spot 2.9.5.dev (not yet released)
|
||||||
- tgba_determinize() could create parity automata using more colors
|
- tgba_determinize() could create parity automata using more colors
|
||||||
than necessary.
|
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)
|
New in spot 2.9.5 (2020-11-19)
|
||||||
|
|
||||||
Bugs fixed:
|
Bugs fixed:
|
||||||
|
|
|
||||||
|
|
@ -933,9 +933,12 @@ namespace spot
|
||||||
{ false, // state based
|
{ false, // state based
|
||||||
false, // inherently_weak
|
false, // inherently_weak
|
||||||
false, false, // deterministic
|
false, false, // deterministic
|
||||||
true, // complete
|
false, // complete
|
||||||
true // stutter inv
|
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.
|
// Given a safra_state get its associated state in output automata.
|
||||||
// Required to create new edges from 2 safra-state
|
// Required to create new edges from 2 safra-state
|
||||||
|
|
|
||||||
|
|
@ -25,9 +25,16 @@ a1 = spot.automaton("""genltl --dac=51 | ltl2tgba --med |""")
|
||||||
a1 = spot.degeneralize_tba(a1)
|
a1 = spot.degeneralize_tba(a1)
|
||||||
r1 = spot.tgba_determinize(a1, True, False, False)
|
r1 = spot.tgba_determinize(a1, True, False, False)
|
||||||
assert r1.num_sets() == 3
|
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.automaton("""genltl --dac=51 | ltl2tgba --high |""")
|
||||||
a2 = spot.degeneralize_tba(a2)
|
a2 = spot.degeneralize_tba(a2)
|
||||||
r2 = spot.tgba_determinize(a2, True, False, False)
|
r2 = spot.tgba_determinize(a2, True, False, False)
|
||||||
# This used to fail in 2.9.5 and earlier.
|
# This used to fail in 2.9.5 and earlier.
|
||||||
assert r2.num_sets() == 3
|
assert r2.num_sets() == 3
|
||||||
|
assert a2.prop_complete().is_false();
|
||||||
|
assert r2.prop_complete().is_maybe();
|
||||||
|
assert spot.is_complete(r2)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue