• Alexandre Duret-Lutz's avatar
    introduce is_obligation(f) · 50fe34a5
    Alexandre Duret-Lutz authored
    This is not optimal yet because it still construct a minimal WDBA
    internally, but it's better than the previous way to call
    minimize_obligation() since it can avoid constructing the minimized
    automaton in a few more cases.
    * spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
    * bin/ltlfilt.cc: Wire it to --obligation.
    * spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
    needed by the above.
    * tests/core/obligation.test: Test it.
    * bin/man/spot-x.x, NEWS: Document it.