* spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
function.
* python/spot/__init__.py: Also make it a method of formula in Python
* bin/common_output.cc, bin/common_output.hh: Implement
--stats=%[OP]n.
* NEWS: Mention it.
* tests/core/format.test, tests/python/formulas.ipynb: Test it.
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
is_obligation().
* 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.
* spot/tl/hierarchy.cc (is_recurrence): Do not request state-based
acceptance, now that the Rabin->DBA conversionn works on
transition-based acceptance as well.
For #212.
* spot/twa/twa.hh: Rename prop_deterministic() as prop_universal(),
and keep the old name as deprecated.
* spot/twaalgos/isdet.cc, spot/twaalgos/isdet.hh: Rename
is_deterministic() as is_universal(), and add a new function
for is_deterministic().
* doc/org/concepts.org, doc/org/hoa.org, doc/org/tut21.org,
spot/tl/hierarchy.cc, spot/twa/twagraph.cc,
spot/twaalgos/are_isomorphic.cc, spot/twaalgos/determinize.cc,
spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/hoa.cc, spot/twaalgos/minimize.cc,
spot/twaalgos/postproc.cc, spot/twaalgos/product.cc,
spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/word.cc, tests/python/product.ipynb,
tests/python/remfin.py: Adjust.
* NEWS: Mention the change.
* bin/common_output.cc: Move some of the printing code...
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new
variants of mp_class...
* python/spot/impl.i: ... that we can now call from Python.
* python/ajax/spotcgi.in: Use those to simplify and extend
the code printing class membership.
* spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
terminal SCCs that are incomplete, as if they had a non-accepting
sink as successor.
* spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
(is_terminal_automaton): Add an option to ignore trivial SCC as we did
before, since it matters for deciding membership to the guarantee
class.
(is_safety_mwdba): Rewrite as ...
(is_safety_automaton): ... generalizating to any acceptance, and
ignoring trivial SCCs.
* bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
is_safety_automaton().
* tests/core/hierarchy.test: Add a problematic formula as test-case.
* NEWS: Mention the bug.
Tools for deciding the class of a formula.
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/common_output.cc, bin/common_output.hh: Implement --format=%h.
* tests/core/hierarchy.test: More tests.
* NEWS: Update.
