-
Alexandre Duret-Lutz authored
This makes dstar2tgba able to produce a minimal WDBA when the input DRA represent an obligation property. * src/tgbaalgos/minimize.cc (minimize_obligation): When the formula is not supplied but the input automaton is deterministic, complement it to check the result of WDBA minimization. * src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve tests.
2dda2c91