* NEWS, configure.ac, doc/org/setup.org: Update version and date.

As discussed at https://github.com/adl/hoaf/issues/56

* src/parseaut/scanaut.ll: Allow dots.
* src/tests/parseaut.test: Test it.
* NEWS: Mention it.

* src/twaalgos/word.hh, src/twaalgos/word.cc: Store the
bdd_dict, and replace the print() method by a << overload.
* NEWS: Mention it.
* src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust.

Fixes #4 and fixes #5.

* NEWS: Mention the change.
* src/kripkeparse/: Delete.
* README, src/Makefile.am, configure.ac: Adjust.
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: Delete.
* src/kripke/kripkegraph.hh: New file.
* src/kripke/Makefile.am: Adjust.
* src/parseaut/parseaut.yy, src/parseaut/public.hh: Add
an option to read kripke structures.
* src/tests/bad_parsing.test: Delete.
* src/tests/Makefile.am: Adjust.
* src/tests/kripke.test, src/tests/parse_print_test.cc: Rewrite.
* src/tests/ikwiad.cc, src/tests/parseaut.test,
iface/ltsmin/modelcheck.cc, wrap/python/spot_impl.i: Adjust.

* src/twaalgos/hoa.cc, src/twaalgos/hoa.hh: Implement it.
* NEWS, doc/org/hoa.org, src/bin/common_aoutput.cc: Document it.
* src/tests/readsave.test: Test it.

* src/twaalgos/dtwasat.cc: Choose the reference automaton based on its
size.  With this change, the last example of my LPAR'15 talk goes from
~7s to under 1s.
* NEWS: Mention it.

* src/twaalgos/dtgbasat.cc, src/twaalgos/dtgbasat.hh: Rename as...
* src/twaalgos/dtwasat.cc, src/twaalgos/dtwasat.hh: ... these.
* src/bin/autfilt.cc, src/tests/ikwiad.cc, src/twaalgos/Makefile.am,
src/twaalgos/postproc.cc, wrap/python/spot_impl.i: Adjust.
* NEWS: Mention the renamings.

* NEWS: Mention it.
* wrap/python/spot.py: Rewrite the sat_minimize() function.
* wrap/python/tests/satmin.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.

* src/twaalgos/dot.cc: Here.
* NEWS, src/bin/common_aoutput.cc: Document it.
* wrap/python/tests/automata.ipynb: Test it.

* src/twaalgos/dot.cc: Here.
* wrap/python/tests/automata.ipynb: Test it.
* NEWS: Document this.

* NEWS: Mention the fixed bug.
* src/twaalgos/dot.cc: Fix.
* wrap/python/tests/decompose.ipynb: Use it.

Fixes #122.

* src/twaalgos/word.cc, src/twaalgos/word.hh: Here.
* src/bin/ltlcross.cc, src/bin/common_aoutput.hh: Adjust.
* NEWS: Mention the renaming.

* wrap/python/tests/decompose.ipynb: New file.
* wrap/python/tests/Makefile.am: Add it.
* src/twaalgos/strength.cc: Fix corner cases.
* src/tests/strength.test: Adjust corner case.
* NEWS, doc/org/tut.org: Mention the notebook.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(decompose_stregth): New function.
* src/bin/autfilt.cc: Add a --decompose-strength option.
* src/bin/man/autfilt.x: Add bibliography.
* src/tests/strength.test: Test it.
* NEWS: Mention it.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh (check_strength):
New function.
* src/bin/common_aoutput.cc: Add --check=strength.
* src/tests/strength.test: New file.
* src/tests/Makefile.am: Add it.
* doc/org/hoa.org, NEWS: Document it.

Fixes #47.

* src/twaalgos/strength.cc, src/twaalgos/strength.hh
(is_weak_automaton): New function.
(is_terminal_automaton): Generalize slightly.
* src/bin/autfilt.cc: Add options --is-terminal and --is-weak.
* src/tests/readsave.test: Add a test.
* NEWS: Update.

* src/twaalgos/safety.hh, src/twaalgos/safety.cc: Here.
* src/bin/ltlfilt.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
wrap/python/ajax/spotcgi.in: Adjust.
* NEWS: Mention the change.

* src/twa/twa.hh: Store the terminal property.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O for "terminal".
* src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/minimize.cc: Set terminal
as apropriate.
* src/twaalgos/safety.cc: Use it.
* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/tests/complement.test, src/tests/monitor.test,
wrap/python/tests/automata-io.ipynb: Adjust.

This fixes #119.

* doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it.
* src/twa/twa.hh: Support it in automata.
* src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O support.
* src/twaalgos/minimize.cc, src/twaalgos/totgba.cc: Set weak
automata on output.
* src/tests/complement.test, src/tests/parseaut.test,
src/tests/readsave.test, src/tests/remfin.test, src/tests/sccsimpl.test,
src/tests/wdba2.test, wrap/python/tests/automata-io.ipynb: Adjust.

* src/twaalgos/hoa.cc: Output do not output "unambiguous" if the
automaton is deterministic.  Add option "v" to cancel this restriction,
and also output "no-univ-branch".
* src/twaalgos/hoa.hh: Document the "v" option.
* src/tests/readsave.test: Test it.
* src/tests/unambig.test: Adjust for unambiguous not being output
if the automaton is deterministic.
* src/bin/common_aoutput.cc, NEWS: Document it.
* doc/org/hoa.org: Add a summary table about how properties are handled.
* src/twa/twa.hh (prop_deterministic): Setting this should also
set the unambiguous property.
* src/twaalgos/isunamb.cc: Simplify the property check.

Fixes #117.

* wrap/python/spot.py, wrap/python/spot_impl.i: Add binding.
* wrap/python/tests/remfin.py: Add a small test case.
* NEWS: Mention it.

This fixes #116.

* src/twa/twa.hh: Rename those methods.
* NEWS: Document the renamings.
* doc/org/hoa.org, doc/org/tut21.org, src/parseaut/parseaut.yy,
src/tests/ikwiad.cc, src/twa/twagraph.hh,
src/twaalgos/are_isomorphic.cc, src/twaalgos/complete.cc,
src/twaalgos/degen.cc, src/twaalgos/dot.cc, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/isdet.cc,
src/twaalgos/isunamb.cc, src/twaalgos/lbtt.cc,
src/twaalgos/minimize.cc, src/twaalgos/postproc.cc,
src/twaalgos/product.cc, src/twaalgos/randomgraph.cc,
src/twaalgos/remfin.cc, src/twaalgos/sbacc.cc,
src/twaalgos/simulation.cc, src/twaalgos/stutter.cc,
src/twaalgos/totgba.cc: Adjust.

Fixes #115.

* src/parseaut/parseaut.yy: Set the property on the output automaton.
* src/tests/unambig.test: Add a test case.
* NEWS: Mention the fix.

* NEWS, configure.ac, doc/org/setup.org: Update version.

* src/twa/twa.hh, src/ta/ta.hh (current_state,
current_acceptance_conditions, current_condition): Rename as...
(dst, acc, cond): ... these.
* iface/ltsmin/ltsmin.cc, src/kripke/fairkripke.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.cc,
src/kripke/kripke.hh, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
src/ta/taproduct.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/dot.cc, src/taalgos/emptinessta.cc,
src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
src/taalgos/tgba2ta.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
src/twa/twagraph.hh, src/twa/twaproduct.cc,
src/twa/twasafracomplement.cc, src/twaalgos/bfssteps.cc,
src/twaalgos/bfssteps.hh, src/twaalgos/compsusp.cc,
src/twaalgos/copy.cc, src/twaalgos/emptiness.cc,
src/twaalgos/gtec/gtec.cc, src/twaalgos/gv04.cc,
src/twaalgos/lbtt.cc, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
src/twaalgos/ndfs_result.hxx, src/twaalgos/reachiter.cc,
src/twaalgos/se05.cc, src/twaalgos/stats.cc,
src/twaalgos/stutter.cc, src/twaalgos/tau03.cc,
src/twaalgos/tau03opt.cc, wrap/python/tests/interdep.py: Adjust.
* NEWS: Mention the renamings.

* src/parseaut/public.hh, src/parseaut/parseaut.yy,
src/parseaut/fmterror.cc: Add a raise_errors options.  Remove the
parse_strict() method.  Store parse errors and filename in the output
parsed_aut to simplify usage.
* doc/org/tut20.org, doc/org/tut21.org, doc/org/tut30.org,
src/bin/autfilt.cc, src/bin/common_hoaread.cc, src/bin/dstar2tgba.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltlcross3.test, src/tests/ltldo.test,
wrap/python/spot.py, wrap/python/tests/parsetgba.py: Adjust usage.
* NEWS: Mention the changes.

These now become twa_run::reduce, twa_run::replay, and
twa_run::as_twa.

* src/twaalgos/reducerun.cc, src/twaalgos/reducerun.hh,
src/twaalgos/replayrun.cc, src/twaalgos/replayrun.hh: Delete.
* src/twaalgos/Makefile.am: Adjust.
* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh: Move
the above functions here, as method of twa_run.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
wrap/python/ajax/spotcgi.in, iface/ltsmin/modelcheck.cc: Adjust.
* NEWS: List the renamings.

Part of #113.

* src/twaalgos/emptiness.cc, src/twaalgos/emptiness.hh (tgba_run):
Rename as ...
(twa_run): ... this.
* NEWS: Mention it.
* iface/ltsmin/modelcheck.cc, src/tests/complementation.cc,
src/tests/emptchk.cc, src/tests/ikwiad.cc, src/tests/randtgba.cc,
src/twa/twa.hh, src/twaalgos/bfssteps.cc, src/twaalgos/bfssteps.hh,
src/twaalgos/gtec/ce.cc, src/twaalgos/gtec/ce.hh,
src/twaalgos/gv04.cc, src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
src/twaalgos/ndfs_result.hxx, src/twaalgos/projrun.cc,
src/twaalgos/projrun.hh, src/twaalgos/reducerun.cc,
src/twaalgos/reducerun.hh, src/twaalgos/replayrun.cc,
src/twaalgos/replayrun.hh, src/twaalgos/se05.cc, src/twaalgos/word.cc,
src/twaalgos/word.hh, wrap/python/ajax/spotcgi.in,
wrap/python/spot_impl.i: Adjust.

* src/taalgos/stats.cc, src/taalgos/stats.hh
(tgba_statistics::transitions, tgba_sub_statistics::sub_transitions):
Rename ...
(twa_statistics::edges, twa_sub_statistics::transitions): ... to
these.
* NEWS: Mention it.
* src/bin/common_aoutput.hh, src/bin/ltlcross.cc,
src/tests/checkta.cc, src/tests/complementation.cc,
src/tests/ikwiad.cc, src/tests/ltl2tgba.test,
src/tests/neverclaimread.test, src/tests/randtgba.cc,
src/tests/renault.test, src/tests/wdba2.test, src/twaalgos/dtbasat.cc,
src/twaalgos/dtgbasat.cc, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, wrap/python/ajax/spotcgi.in: Adjust.

Fixes #114.

* src/parseaut/public.hh: Add support for a trust_hoa option.
* src/parseaut/parseaut.yy: If trust_hoa is set, recognize the
"inherently-weak" and "stutter-invariant" properties.
* src/bin/common_conv.cc, src/bin/common_conv.hh (read_automaton):
Move...
* src/bin/common_hoaread.cc, src/bin/common_hoaread.hh: ... in this
new file, that also handle the --trust-hoa option.
* src/bin/Makefile.am: Add them.
* src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/bin/ltldo.cc: Use them.
* src/tests/parseaut.test, src/tests/ltldo.test: Adjust, and test
--trust-hoa=no.
* src/tests/complement.test, src/tests/prodor.test,
src/tests/sbacc.test: Adjust.
* wrap/python/spot.py (automata): Add option trust_hoa.
* NEWS: Update.

This occured when parsing the HOA automaton generated by Rabinizer3 for
a very long LTL formula with many nested U.  State labels could easily
be more than 40k characters.

* src/parseaut/scanaut.ll: Fix that.
* src/tests/parseaut.test: New test case.
* NEWS: Mention the fix.

* wrap/python/spot.py: Implement it.  Also report non-zero
exit using CalledProcessError.
* wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
Adjust.
* NEWS: Mention the change.

* src/tests/unambig.test: New test case.  Reported by Ming-Hsien Tsai.
* src/twaalgos/sccfilter.cc: Always create an initial state.
* src/twaalgos/isunamb.cc: Speed up on empty languages.
* NEWS, THANKS: Update.

This simplifies the use of the spot.postprocessor object.

* wrap/python/spot.py: Add it.
* wrap/python/tests/automata.ipynb: Use it.
* NEWS: Mention it.

This is a bug:

    % ltlfilt -f 'a W b' --unabbreviate=WR
    a U (b | (a W b))

* src/tl/unabbrev.cc: Here.
* src/tests/unabbrevwm.test: Harden test case.
* wrap/python/tests/randltl.ipynb: Adjust expected output.
* NEWS: Mention the fix.

* wrap/python/spot_impl.i (get_name, set_name): New methods for twa.
* wrap/python/tests/remfin.py: Test them.
* wrap/python/ajax/spotcgi.in: Use set_name().
* NEWS: Mention it.

* doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh,
src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh,
src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc,
src/twaalgos/translate.cc, src/twaalgos/translate.hh,
wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier.
* NEWS: Mention it.

* debian/rules: Build for all supported python3 versions.
* NEWS: Mention it.