Suggested by Jeroen Meijer.

* spot/libspot.pc.in, spot/ltsmin/libspotltsmin.pc.in: New file.
* spot/Makefile.am, spot/ltsmin/Makefile.am: Distribute them, and
install their derived version.
* spot/.gitignore: Ignore *.pc files.
* debian/libbddx-dev.install, debian/libspot-dev.install: Ship
those *.pc files.
* NEWS: Mention it.

* src/libbddx.pc.in: New file.
* src/Makefile.am: Generate libbddx.pc, and install it.
Distribute libbddx.pc.in.
* src/.gitignore: Ignore *.pc.

* bin/ltlcross.cc: Fix it.
* tests/core/ltlcross3.test: Test it.
* NEWS: Mention the bug.

Fixes #204.

* spot/twaalgos/dtwasat.cc (sat_minimize): Here.
* tests/core/satmin2.test: Add a test case.
* NEWS: Mention the bug.

* spot/twaalgos/alternation.cc: Fix the code to also check the
weakness of single-state SCCs.
* tests/core/alternating.test: Add a test from ltl3hoa.

Suggested by Jeroen Meijer.

* debian/rules: Enable static libraries.
* debian/libbddx-dev.install, debian/libspot-dev.install: Distribute
them.
* THANKS: Add Jeroen.
* NEWS: Mention the change.

* bin/common_trans.cc: Add shorthand for ltl3hoa.
* NEWS, doc/org/ltlcross.org, doc/org/ltldo.org: Mention it.

* bin/common_trans.cc, bin/common_trans.hh: Add the --relabel option.
* bin/ltlcross.cc, bin/ltldo.cc: Implement it.
* doc/org/ltldo.org, NEWS: Document it.
* tests/core/ltl3ba.test: Test it.

* bin/ltlcross.cc: Do it.
* bin/common_trans.cc: Adjust documentation.
* tests/core/ltl3ba.test: Test it.
* NEWS: Document it.

* doc/org/hierarchy.org, doc/org/hierarchy.tex: New files.
* doc/Makefile.am, doc/org/tools.org, NEWS: Add them.

* doc/org/ltlfilt.org: Update example.
* doc/org/ioltl.org: Explain %s briefly.

* 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.

* spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh
(rabin_to_buchi_maybe): Make this function public.
* bin/ltlfilt.cc: Implement the two options.
* tests/core/hierarchy.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new options.

* tests/core/alternating.test: Run some of the test through
valgrind to exhibit the bug.
* spot/twa/twagraph.cc: Fix it.

* bench/dtgbasat/config.bench: Configuration file sample used by gen.py
* bench/dtgbasat/gen.py: Script that can generate both bench script and
pdf results.
* bench/dtgbasat/stats.sh: Change stat.sh into stat-gen.sh that will be
generated by gen.py script.
* bench/dtgbasat/Makefile.am: Add new files.
* bench/dtgbasat/README: Update README.
* bench/dtgbasat/stat-gen.sh: Add stat script generated by gen.py and
default config.bench file.

* NEWS: Update.
* doc/org/satmin.org: Update satmin page.
* bin/man/spot-x.x: Document SPOT_XCNF and edit SPOT_SATSOLVER.
* bin/spot-x.cc: Update satmin options.
* bin/autfilt.cc: Update satmin related documentations.
* bin/man/autfilt.x: Update autfilt options.

* spot/misc/satsolver.cc: Handle xcnf writing.
* spot/misc/satsolver.hh: Handle xcnf writing.

* python/spot/__init__.py: Handle options.
* spot/twaalgos/dtwasat.cc: Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Handle options.
* tests/core/satmin.test: Update tests.
Now use 'sat-minimize=4' to use the naive algo.
* tests/core/satmin2.test: Update tests.
Now use --sat-minimize='naive' to use the naive algo.
* tests/python/satmin.py: Update tests.
Now use 'naive=True' to use the naive algo.

* python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
* spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
* spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
* spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
* tests/core/satmin2.test: Add tests for dichotomy.
* tests/core/satmin.test: Add tests for dichotomy.
* tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.

* bin/autfilt.cc: Add that option.
* tests/core/highlightstate.test: Add test.
* NEWS: Update.

* python/spot/impl.i: Add python bindings.
* spot/twaalgos/langmap.cc: Implement algo.
* spot/twaalgos/langmap.hh: Declare algo.
* spot/twaalgos/Makefile.am: Add new files.
* tests/python/langmap.py: Add tests.
* NEWS: Update.

* python/spot/__init__.py: Add 'assume' option.
* spot/misc/satsolver.cc: Add function to handle assumptions.
* spot/misc/satsolver.hh: Declare assumption function.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_assume.
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_assume and
handle options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Use param_ var for incr and assume.
* tests/core/satmin.test: Add tests for the new function.
* tests/core/satmin2.test: Add tests for the new function.
* tests/python/satmin.py: Add tests for the new function.

* python/spot/__init__.py: Add 'incr' boolean argument.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...).
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and
deal with options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Add option --sat-minimize=incr.
* spot/twaalgos/postproc.hh: Add incr parameter.
* tests/core/satmin.test: Add tests for incremental version.
Update expected result.
* tests/core/satmin2.test: Add tests for incremental version.
* tests/python/satmin.py: Add tests for incremental version.

* spot/misc/satsolver.hh: Make solver return vector<bool> instead of
vector<int>.
* spot/misc/satsolver.cc: Update code.
* spot/priv/Makefile.am: Add satcommon.*
* spot/priv/satcommon.hh: Declare helper class and factorize some
duplicate code of dt*asat.cc
* spot/priv/satcommon.cc: Implement helper class and factorize some
duplicate code of dt*asat.cc
* spot/twaalgos/dtbasat.cc: Declare helper, implement some functions
in dict struct and update code.
* spot/twaalgos/dtwasat.cc: Declare helper, implement some functions
in dict struct and update code.
* tests/core/readsat.cc: Update tests.
* tests/core/satmin.test: Typo.
* tests/core/satmin2.test: Update an expected result.

* spot/twaalgos/dtbasat.cc: Fix static sat_build.
* spot/twaalgos/dtwasat.cc: Fix static sat_build.

* tests/core/satmin.test: Delete check for SPOT_SATSOLVER env
variable and add state numbers verification.
* tests/core/satmin2.test: Delete check for SPOT_SATSOLVER
env variable.
* tests/python/satmin.py: Delete check for SPOT_SATSOLVER
env variable.

* Makefile.am: Add picosat to subdirs.
* configure.ac: Add picosat/Makefile to AC_CONFIG_FILES.
* README: Add picosat/ in the list of directories.
* debian/copyright: Add picosat licence and details.
* picosat/Makefile.am: Implement Makefile.am in picosat directory.
* spot/Makefile.am: Tell the compiler to add libpico.la into libspot.la.
* picosat/LICENSE: Add picosat licence.
* picosat/NEWS: Add picosat NEWS.
* picosat/VERSION: Add picosat VERSION.
* picosat/picosat.c: Add picosat c file.
* picosat/picosat.h: Add picosat header file.
* spot/misc/satsolver.cc: Update functions.
* spot/misc/satsolver.hh: Add documentation, clean code, change
some functions visibility and separate templates functions.
* spot/twaalgos/dtbasat.cc: Update dtba_to_sat function.
* spot/twaalgos/dtwasat.cc: Update dtwa_to_sat function.

* spot/misc/satsolver.hh: Declare all functions needed.
* spot/misc/satsolver.cc: Implement them.
* spot/twaalgos/dtbasat.cc: Abstract writing.
* spot/twaalgos/dtwasat.cc: Abstract writing.

* .gitignore: Fix typo dt*a instead of dt*ba.

This fix recent failures observed on arch linux because
it uses newer versions of graphviz and Python.

* tests/python/ipnbdoctest.py (sanitize): More substitutions.

* bin/common_setup.cc: Here.

Algorithms that remove transitions can turn a non-deterministic
automaton into a deterministic one, so we need to be able to specify
that determinism can be improved (as opposed to preserved).

* spot/twa/twa.hh (twa::prop_set::improve_det): New attribute.
(twa::prop_keep, twa::prop_copy): Honor it.
* spot/tl/exclusive.cc, spot/twaalgos/alternation.cc,
spot/twaalgos/complete.cc, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/mask.cc,
spot/twaalgos/minimize.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
spot/twaalgos/sccfilter.cc, spot/twaalgos/simulation.cc,
spot/twaalgos/strength.cc, spot/twaalgos/stutter.cc,
spot/twaalgos/totgba.cc: Adjust calls to prop_keep() and
prop_copy().

* spot/twaalgos/simulation.cc: Reset those to maybe.
* tests/core/semidet.test: Add some tests.

* spot/twa/twa.hh (prop_semi_deterministic): New methods.
* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
semi-deterministic property.
* doc/org/concepts.org, doc/org/hoa.org: Document it.
* spot/twaalgos/isdet.cc,
spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
* bin/autfilt.cc: Add --is-semi-deterministic.
* bin/common_aoutput.cc: Add --check=semi-deterministic.
* tests/core/semidet.test: New file.
* tests/Makefile.am: Add it.
* tests/core/parseaut.test, tests/core/readsave.test: Adjust.

* spot/graph/graph.hh (internal::univ_dest_mapper): New helper class.
* spot/twa/twagraph.cc (merge_univ_dests): Simplify using
univ_dest_mapper.
(purge_unreachable_states, purge_dead_states): Add support for
alternation.
* tests/core/alternating.test: More tests.

* bin/autfilt.cc (ensure_deterministic): Remove alternation on demand.
(process_automaton): Prefer twa::intersects() over
product()/is_empty().
* spot/twa/twa.cc (remove_fin_maybe): Also remove alternation.
* tests/core/alternating.test: More tests.