GitLab

* src/twa/bddprint.cc: Do not store a global shared_ptr to the bdddict
used for printing (a simple pointer is enough), otherwise it risks being
the last shared_ptr to be destroyed, and it might be destroyed after the
unicity maps of the formulas.

* NEWS: Mention it.
* bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, doc/mainpage.dox,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc,
src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh, src/bin/common_r.hh,
src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.cc,
src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/parseaut/parseaut.yy,
src/parseaut/public.hh, src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
src/tests/ltlrel.cc, src/tests/parse.test,
src/tests/parse_print_test.cc, src/tests/randtgba.cc,
src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
src/tests/taatgba.cc, src/tests/tostring.cc, src/tests/tostring.test,
src/tl/apcollect.cc, src/tl/apcollect.hh, src/tl/contain.cc,
src/tl/contain.hh, src/tl/declenv.cc, src/tl/declenv.hh,
src/tl/defaultenv.cc, src/tl/defaultenv.hh, src/tl/dot.cc,
src/tl/dot.hh, src/tl/environment.hh, src/tl/exclusive.cc,
src/tl/exclusive.hh, src/tl/formula.cc, src/tl/formula.hh,
src/tl/length.cc, src/tl/length.hh, src/tl/mark.cc, src/tl/mark.hh,
src/tl/mutation.cc, src/tl/mutation.hh, src/tl/nenoform.cc,
src/tl/nenoform.hh, src/tl/print.cc, src/tl/print.hh,
src/tl/randomltl.cc, src/tl/randomltl.hh, src/tl/relabel.cc,
src/tl/relabel.hh, src/tl/remove_x.cc, src/tl/remove_x.hh,
src/tl/simpfg.cc, src/tl/simpfg.hh, src/tl/simplify.cc,
src/tl/simplify.hh, src/tl/snf.cc, src/tl/snf.hh, src/tl/unabbrev.cc,
src/tl/unabbrev.hh, src/twa/bdddict.cc, src/twa/bdddict.hh,
src/twa/bddprint.cc, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.hh,
src/twa/twagraph.cc, src/twa/twagraph.hh, src/twaalgos/compsusp.cc,
src/twaalgos/compsusp.hh, src/twaalgos/ltl2taa.cc,
src/twaalgos/ltl2taa.hh, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/minimize.cc,
src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
src/twaalgos/postproc.cc, src/twaalgos/postproc.hh,
src/twaalgos/powerset.cc, src/twaalgos/powerset.hh,
src/twaalgos/randomgraph.cc, src/twaalgos/randomgraph.hh,
src/twaalgos/relabel.cc, src/twaalgos/relabel.hh,
src/twaalgos/remprop.cc, src/twaalgos/remprop.hh, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh,
src/twaalgos/translate.cc, src/twaalgos/translate.hh,
wrap/python/spot_impl.i: Remove the ltl namespace.

The ltl prefix does not make a lot of sens anymore (since we
support psl as well).  ltlast/ and ltlenv/ were almost empty.
And ltlvisit/ did not contain any visitor anymore.

* src/ltlvisit/, src/ltlast/, src/ltlenv/: Merge into...
* src/tl/: ...this.
* NEWS: Mention the change.
* README, bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, src/Makefile.am,
src/bin/autfilt.cc, src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_r.hh, src/bin/common_trans.cc, src/bin/genltl.cc,
src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc,
src/bin/randltl.cc, src/kripke/kripkeexplicit.hh,
src/kripkeparse/public.hh, src/parseaut/public.hh, src/priv/accmap.hh,
src/ta/taexplicit.hh, src/ta/tgtaexplicit.hh, src/tests/equalsf.cc,
src/tests/ikwiad.cc, src/tests/length.cc, src/tests/ltlrel.cc,
src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc,
src/tests/syntimpl.cc, src/tests/taatgba.cc, src/tests/tostring.cc,
src/tests/twagraph.cc, src/twa/acc.hh, src/twa/bdddict.cc,
src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/taatgba.cc,
src/twa/taatgba.hh, src/twa/twa.hh, src/twa/twagraph.cc,
src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc,
src/twaalgos/isweakscc.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
src/twaalgos/randomgraph.hh, src/twaalgos/relabel.hh,
src/twaalgos/remprop.hh, src/twaalgos/stats.cc, src/twaalgos/stutter.cc,
src/twaalgos/translate.hh, wrap/python/spot_impl.i,
src/ltlparse/ltlparse.yy, src/ltlparse/public.hh: Adjust.

Fixes #106.

* m4/gccwarn.m4: Use -Wzero-as-null-pointer-constant if supported.
* src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_post.cc, src/bin/common_r.hh, src/bin/common_range.hh,
src/bin/common_setup.cc, src/bin/common_trans.cc, src/bin/dstar2tgba.cc,
src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc,
src/bin/spot-x.cc, src/kripke/kripkeexplicit.cc, src/ltlast/formula.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/snf.hh, src/misc/fixpool.hh,
src/misc/mspool.hh, src/misc/hash.hh, src/misc/optionmap.cc,
src/misc/satsolver.cc, src/misc/tmpfile.cc, src/misc/tmpfile.hh,
src/priv/bddalloc.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/tgtaexplicit.hh,
src/ta/tgtaproduct.cc, src/taalgos/minimize.cc,
src/taalgos/reachiter.cc, src/taalgos/tgba2ta.cc,
src/tests/complementation.cc, src/tests/ikwiad.cc,
src/tests/randtgba.cc, src/tests/reduc.cc, src/twa/bdddict.cc,
src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/twa.cc,
src/twa/twagraph.hh, src/twa/twaproduct.cc,
src/twa/twasafracomplement.cc, src/twaalgos/bfssteps.cc,
src/twaalgos/compsusp.cc, src/twaalgos/dtgbasat.cc,
src/twaalgos/emptiness.cc, src/twaalgos/gtec/ce.cc,
src/twaalgos/gv04.cc, src/twaalgos/ltl2taa.cc,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
src/twaalgos/magic.cc, src/twaalgos/minimize.cc,
src/twaalgos/ndfs_result.hxx, src/twaalgos/postproc.cc,
src/twaalgos/postproc.hh, src/twaalgos/reachiter.cc,
src/twaalgos/reducerun.cc, src/twaalgos/safety.hh,
src/twaalgos/sccfilter.hh, src/twaalgos/se05.cc,
src/twaalgos/simulation.cc, src/twaalgos/tau03.cc,
src/twaalgos/tau03opt.cc, src/twaalgos/translate.cc,
src/twaalgos/translate.hh, utf8/utf8/core.h,
bench/stutter/stutter_invariance_formulas.cc, iface/ltsmin/ltsmin.cc,
iface/ltsmin/modelcheck.cc: Use nullptr to fix the warning.

Flatten the formula ltl::formula hiearchy into a single ltl::vnode that
has an enumerator to distinguish the types of node, and a common
interface to access children, update reference counts, etc.  The
ltl::formula class is now a thin wrapper around an ltl::vnode pointer to
keep track of reference counts automatically.  Visitor are not used
anymore; we now have map() and traversor() methods that are more
concise.

This basically fixes #43, but should be followed by some fine tuning
that should now be localized to the formula.hh and formula.cc files.

Some statistics about this patch.  I started working on it on Sep 9, had
a first compiling version two weeks later on Sep 22, and it then took 5
days to fixes the ~70 distincts bugs that were introduced during the
conversion.  About 13200 lines were modified, and one third of those
were removed.

* src/ltlast/formula.cc, src/ltlast/formula.hh: Complete rewrite,
including what was in separate nearby files.
* src/ltlast/allnodes.hh, src/ltlast/atomic_prop.cc,
src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh,
src/ltlast/bunop.cc, src/ltlast/bunop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlvisit/dump.cc,
src/ltlvisit/dump.hh, src/ltlast/predecl.hh: Delete these files.  Their
feature have been merged in formula.hh and formula.cc.
* src/ltlast/visitor.hh, src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
src/ltlvisit/dump.hh, src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh:
Delete these files, as we do not use visitors anymore.
* bench/stutter/stutter_invariance_formulas.cc,
bench/stutter/stutter_invariance_randomgraph.cc, doc/org/tut01.org,
doc/org/tut02.org, doc/org/tut10.org, doc/org/tut22.org,
iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc,
src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.cc,
src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripkeparse/kripkeparse.yy, src/ltlast/Makefile.am,
src/ltlenv/declenv.cc, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
src/ltlparse/ltlparse.yy, src/ltlparse/public.hh,
src/ltlvisit/Makefile.am, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/dot.cc, src/ltlvisit/dot.hh,
src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh,
src/ltlvisit/length.cc, src/ltlvisit/length.hh, src/ltlvisit/mark.cc,
src/ltlvisit/mark.hh, src/ltlvisit/mutation.cc,
src/ltlvisit/mutation.hh, src/ltlvisit/nenoform.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/print.cc, src/ltlvisit/print.hh,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh,
src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh,
src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc,
src/ltlvisit/snf.hh, src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh,
src/parseaut/parseaut.yy, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
src/taalgos/minimize.cc, src/taalgos/tgba2ta.cc, src/tests/bare.test,
src/tests/checkpsl.cc, src/tests/checkta.cc,
src/tests/complementation.cc, src/tests/consterm.cc,
src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
src/tests/isop.test, src/tests/kind.cc, src/tests/length.cc,
src/tests/ltldo.test, src/tests/ltlfilt.test, src/tests/ltlgrind.test,
src/tests/ltlprod.cc, src/tests/ltlrel.cc,
src/tests/parse_print_test.cc, src/tests/parseaut.test,
src/tests/parseerr.test, src/tests/randtgba.cc, src/tests/readltl.cc,
src/tests/reduc.cc, src/tests/syntimpl.cc, src/tests/taatgba.cc,
src/tests/tostring.cc, src/tests/twagraph.cc, src/tests/utf8.test,
src/twa/acc.cc, src/twa/bdddict.cc, src/twa/bdddict.hh,
src/twa/bddprint.cc, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twa.hh
src/twa/twagraph.cc, src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
src/twaalgos/minimize.cc, src/twaalgos/minimize.hh,
src/twaalgos/neverclaim.cc, src/twaalgos/postproc.cc,
src/twaalgos/postproc.hh, src/twaalgos/powerset.cc,
src/twaalgos/powerset.hh, src/twaalgos/randomgraph.cc,
src/twaalgos/remprop.cc, src/twaalgos/remprop.hh, src/twaalgos/stats.cc,
src/twaalgos/stats.hh, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh,
src/twaalgos/translate.cc, src/twaalgos/translate.hh,
wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
wrap/python/spot_impl.i, wrap/python/Makefile.am,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/formulas.ipynb,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py, wrap/python/tests/randltl.ipynb: Adjust
to use the new interface.
* src/sanity/style.test: Accept more C++11 patterns.
* NEWS: Mention the change.

This actually performs three related changes, but separating them
would be quite inconvenient.

1) rename tostring.hh to print.hh a welcome side-effect is that
I could fix several files that included this file for not reason.

2) de-overload some of the to_string functions, and rename them
as follow:

  to_string -> print_psl, print_sere, str_psl, str_sere
  to_utf8_string -> print_utf8_psl, print_utf8_sere,
                    str_utf8_psl, str_utf8_sere
  to_spin_string -> print_spin_ltl, str_spin_ltl
  to_wring_string -> print_wring_ltl, str_wing_ltl
  to_lbt_string -> print_lbt_ltl, str_lbt_ltl
  to_latex_string -> print_latex_psl, str_latex_psl
  to_sclatex_string -> print_sclatex_psl, str_sclatex_psl

Now it is clearer what these functions do, and their restrictions.

3) all those print_* functions now take the stream to write onto
as their first argument.  This fixes #88.

* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Rename into...
* src/ltlvisit/print.cc, src/ltlvisit/print.hh: ... those, and make
the changes listed above.
* doc/org/tut01.org, src/bin/common_output.cc,
src/bin/common_trans.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
src/bin/randltl.cc, src/ltlparse/ltlparse.yy,
src/ltlvisit/Makefile.am, src/ltlvisit/mark.cc,
src/ltlvisit/relabel.cc, src/ltlvisit/simplify.cc,
src/ltlvisit/snf.cc, src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
src/taalgos/tgba2ta.cc, src/tests/equalsf.cc, src/tests/ltl2tgba.cc,
src/tests/ltlrel.cc, src/tests/randtgba.cc, src/tests/reduc.cc,
src/tests/syntimpl.cc, src/tests/tostring.cc, src/twa/bdddict.cc,
src/twa/bddprint.cc, src/twa/taatgba.cc, src/twa/taatgba.hh,
src/twa/twagraph.cc, src/twaalgos/compsusp.cc, src/twaalgos/lbtt.cc,
src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2tgba_fm.cc,
src/twaalgos/neverclaim.cc, src/twaalgos/remprop.cc,
src/twaalgos/stats.cc, wrap/python/ajax/spot.in, wrap/python/spot.py,
wrap/python/spot_impl.i: Adjust.

* src/twa/bddprint.cc, src/twa/bddprint.hh (bdd_print_acc,
bdd_print_dot, bdd_print_table): Remove.

Automatic mass renaming.

* src/graphtest/tgbagraph.cc, src/tgba/acc.cc, src/tgba/acc.hh,
src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.hh, src/tgba/fwd.hh, src/tgba/Makefile.am,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgba.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/.cvsignore: Rename as...
* src/graphtest/twagraph.cc, src/twa/acc.cc, src/twa/acc.hh,
src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc,
src/twa/bddprint.hh, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
src/twa/fwd.hh, src/twa/Makefile.am, src/twa/taatgba.cc,
src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twagraph.cc,
src/twa/twagraph.hh, src/twa/twa.hh, src/twa/twamask.cc,
src/twa/twamask.hh, src/twa/twaproduct.cc, src/twa/twaproduct.hh,
src/twa/twaproxy.cc, src/twa/twaproxy.hh,
src/twa/twasafracomplement.cc, src/twa/twasafracomplement.hh,
src/twa/.cvsignore: ... these.
* README, bench/stutter/stutter_invariance_randomgraph.cc,
configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
src/bin/common_aoutput.cc, src/bin/common_conv.hh,
src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc,
src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/public.hh, src/graphtest/Makefile.am,
src/graphtest/ngraph.cc, src/hoaparse/hoaparse.yy,
src/hoaparse/public.hh, src/kripke/fairkripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/exclusive.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/priv/accmap.hh, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/canonicalize.cc,
src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh,
src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.hh,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc,
src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh,
src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc,
src/tgbaalgos/product.hh, src/tgbaalgos/projrun.cc,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh,
src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.cc,
src/tgbaalgos/sccinfo.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaalgos/stripacc.hh,
src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
src/tgbaalgos/weight.hh, src/tgbaalgos/word.cc, src/tgbatest/acc.cc,
src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/taatgba.cc,
wrap/python/spot_impl.i: Adjust.

* iface/dve2/dve2.cc, iface/dve2/dve2.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
src/tgba/tgbagraph.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/translate.cc,
src/tgbaalgos/translate.hh, src/tgbaalgos/word.cc,
src/tgbaalgos/word.hh: Pass shared_ptr to functions by const ref.

* src/tgba/bdddict.hh (bdd_dict_ptr): New type.
(make_bdd_dict): New function.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/dstarparse/dstarparse.yy, src/dstarparse/public.hh,
src/graphtest/tgbagraph.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/neverparse/neverclaimparse.yy, src/neverparse/public.hh,
src/priv/accmap.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/sabatest/sabacomplementtgba.cc,
src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/taalgos/dotty.cc, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh,
src/tgba/wdbacomp.cc, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaalgos/word.cc, src/tgbaalgos/word.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/maskacc.cc,
src/tgbatest/powerset.cc, src/tgbatest/randtgba.cc,
src/tgbatest/taatgba.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/parsetgba.py: Update to use bdd_dict_ptr and
make_bdd_dict().

These were only used by the BDD-based implementation of TGBA, which has
been removed.

* src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc: Remove
support for now/next variables.

* src/sanity/style.test: Add a test.
* iface/dve2/dve2.cc, iface/dve2/dve2check.cc, src/bin/common_output.cc,
src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc,
src/dstarparse/dra2ba.cc, src/dstarparse/fmterror.cc,
src/dstarparse/nsa2tgba.cc, src/kripke/kripkeprint.cc,
src/kripkeparse/fmterror.cc, src/ltlast/atomic_prop.cc,
src/ltlast/bunop.cc, src/ltltest/ltlrel.cc, src/ltltest/reduc.cc,
src/ltltest/syntimpl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/relabel.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/misc/bitvect.cc,
src/misc/optionmap.cc, src/misc/timer.cc, src/neverparse/fmterror.cc,
src/priv/freelist.cc, src/saba/sabacomplementtgba.cc,
src/sabaalgos/sabadotty.cc, src/taalgos/dotty.cc,
src/taalgos/minimize.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc,
src/tgba/futurecondcol.cc, src/tgba/taatgba.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/cycles.cc,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/weight.cc, src/tgbaalgos/word.cc,
src/tgbaparse/fmterror.cc, src/tgbatest/bitvect.cc,
src/tgbatest/complementation.cc, src/tgbatest/intvcmp2.cc,
src/tgbatest/intvcomp.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc: Replace << "c" by << 'c' when
appropriate.

Thomas Badie authored Sep 27, 2012 and Alexandre Duret-Lutz committed Apr 09, 2013

* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Add bdd_print_isop
that prints the bdd into a Irreductible Sum Of Product.
* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Add a way to
know which states (in the input) is which (in the result).
* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Add
the Don't Care Simulation and the Don't Care Iterated Simulation.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/spotlbtt.test,
src/tgbatest/Makefile.am, src/tgbatest/sim.test: Test them.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/README,
bench/ltl2tgba/algorithms: Add a way to bench the don't care
simulation.

* NEWS: Mention this.
* COPYING: Replace by GPL v3.
* src/sanity/style.test: Check files with the wrong license,
in case we forgot to update it during a merge.
* Makefile.am, bench/Makefile.am, bench/emptchk/Makefile.am,
bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh,
bench/emptchk/pml-eeaean.sh, bench/emptchk/pml2tgba.pl,
bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known,
bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small,
bench/ltlclasses/Makefile.am, bench/ltlclasses/defs.in,
bench/ltlclasses/run, bench/ltlcounter/Makefile.am,
bench/ltlcounter/defs.in, bench/ltlcounter/run,
bench/scc-stats/Makefile.am, bench/scc-stats/stats.cc,
bench/split-product/Makefile.am, bench/split-product/cutscc.cc,
bench/split-product/pml2tgba.pl, bench/wdba/Makefile.am,
bench/wdba/defs.in, bench/wdba/run, configure.ac, doc/Makefile.am,
doc/dot.in, doc/tl/Makefile.am, iface/Makefile.am,
iface/dve2/Makefile.am, iface/dve2/defs.in, iface/dve2/dve2.cc,
iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
iface/dve2/dve2check.test, iface/dve2/finite.test,
iface/dve2/kripke.test, iface/gspn/Makefile.am, iface/gspn/common.cc,
iface/gspn/common.hh, iface/gspn/dcswave.test,
iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test,
iface/gspn/dcswaveltl.test, iface/gspn/dottygspn.cc,
iface/gspn/dottyssp.cc, iface/gspn/gspn.cc, iface/gspn/gspn.hh,
iface/gspn/ltlgspn.cc, iface/gspn/simple.test, iface/gspn/ssp.cc,
iface/gspn/ssp.hh, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test,
iface/gspn/udcsfm.test, iface/gspn/udcsltl.test, src/Makefile.am,
src/bin/Makefile.am, src/bin/common_cout.cc, src/bin/common_cout.hh,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_post.cc, src/bin/common_post.hh, src/bin/common_r.cc,
src/bin/common_r.hh, src/bin/common_range.cc, src/bin/common_range.hh,
src/bin/common_setup.cc, src/bin/common_setup.hh,
src/bin/common_sys.hh, src/bin/genltl.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltlfilt.cc, src/bin/man/Makefile.am,
src/bin/randltl.cc, src/eltlparse/Makefile.am,
src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll,
src/eltlparse/fmterror.cc, src/eltlparse/parsedecl.hh,
src/eltlparse/public.hh, src/eltltest/Makefile.am,
src/eltltest/acc.cc, src/eltltest/acc.test, src/eltltest/defs.in,
src/eltltest/nfa.cc, src/eltltest/nfa.test, src/evtgba/Makefile.am,
src/evtgba/evtgba.cc, src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
src/evtgba/explicit.cc, src/evtgba/explicit.hh, src/evtgba/product.cc,
src/evtgba/product.hh, src/evtgba/symbol.cc, src/evtgba/symbol.hh,
src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
src/evtgbaalgos/save.hh, src/evtgbaalgos/tgba2evtgba.cc,
src/evtgbaalgos/tgba2evtgba.hh, src/evtgbaparse/Makefile.am,
src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
src/evtgbatest/readsave.test, src/kripke/Makefile.am,
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/kripke/kripkeprint.hh,
src/kripkeparse/Makefile.am, src/kripkeparse/fmterror.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/kripkescan.ll,
src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh,
src/kripkeparse/scankripke.ll, src/kripketest/Makefile.am,
src/kripketest/bad_parsing.test, src/kripketest/defs.in,
src/kripketest/kripke.test, src/kripketest/parse_print_test.cc,
src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/Makefile.am, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
src/ltlparse/Makefile.am, src/ltlparse/fmterror.cc,
src/ltlparse/ltlfile.cc, src/ltlparse/ltlfile.hh,
src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll,
src/ltlparse/parsedecl.hh, src/ltlparse/public.hh,
src/ltltest/Makefile.am, src/ltltest/consterm.cc,
src/ltltest/consterm.test, src/ltltest/defs.in, src/ltltest/equals.cc,
src/ltltest/equals.test, src/ltltest/kind.cc, src/ltltest/kind.test,
src/ltltest/length.cc, src/ltltest/length.test,
src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/reduc.test,
src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
src/ltltest/tostring.cc, src/ltltest/tostring.test,
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
src/ltltest/utf8.test, src/ltltest/uwrm.test,
src/ltlvisit/Makefile.am, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/lbt.cc,
src/ltlvisit/lbt.hh, src/ltlvisit/length.cc, src/ltlvisit/length.hh,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/mark.cc, src/ltlvisit/mark.hh, src/ltlvisit/nenoform.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.cc,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc,
src/ltlvisit/reduce.hh, src/ltlvisit/relabel.cc,
src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.cc,
src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.cc,
src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc, src/ltlvisit/snf.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
src/misc/Makefile.am, src/misc/acccompl.cc, src/misc/acccompl.hh,
src/misc/accconv.cc, src/misc/accconv.hh, src/misc/bareword.cc,
src/misc/bareword.hh, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/bddlt.hh, src/misc/bddop.cc, src/misc/bddop.hh,
src/misc/casts.hh, src/misc/escape.cc, src/misc/escape.hh,
src/misc/fixpool.hh, src/misc/freelist.cc, src/misc/freelist.hh,
src/misc/hash.hh, src/misc/hashfunc.hh, src/misc/intvcmp2.cc,
src/misc/intvcmp2.hh, src/misc/intvcomp.cc, src/misc/intvcomp.hh,
src/misc/ltstr.hh, src/misc/memusage.cc, src/misc/memusage.hh,
src/misc/minato.cc, src/misc/minato.hh, src/misc/modgray.cc,
src/misc/modgray.hh, src/misc/mspool.hh, src/misc/optionmap.cc,
src/misc/optionmap.hh, src/misc/random.cc, src/misc/random.hh,
src/misc/timer.cc, src/misc/timer.hh, src/misc/unique_ptr.hh,
src/misc/version.cc, src/misc/version.hh, src/neverparse/Makefile.am,
src/neverparse/fmterror.cc, src/neverparse/neverclaimparse.yy,
src/neverparse/neverclaimscan.ll, src/neverparse/parsedecl.hh,
src/neverparse/public.hh, src/saba/Makefile.am,
src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/Makefile.am, src/sabatest/defs.in,
src/sabatest/sabacomplementtgba.cc, src/sanity/Makefile.am,
src/sanity/readme.test, src/sanity/style.test, src/ta/Makefile.am,
src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/taproduct.hh,
src/ta/tgta.cc, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/Makefile.am, src/taalgos/dotty.cc, src/taalgos/dotty.hh,
src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
src/taalgos/tgba2ta.hh, src/tgba/Makefile.am, src/tgba/bdddict.cc,
src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
src/tgba/public.hh, src/tgba/sba.hh, src/tgba/state.hh,
src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiter.hh,
src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc,
src/tgba/wdbacomp.hh, src/tgbaalgos/Makefile.am,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh,
src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/eltl2tgba_lacim.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/gtec/Makefile.am,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc,
src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/tau03opt.hh, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
src/tgbatest/babiak.test, src/tgbatest/bddprod.test,
src/tgbatest/complementation.cc, src/tgbatest/complementation.test,
src/tgbatest/cycles.test, src/tgbatest/defs.in,
src/tgbatest/degendet.test, src/tgbatest/degenid.test,
src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
src/tgbatest/eltl2tgba.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/emptchkr.test,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.cc,
src/tgbatest/explprod.test, src/tgbatest/intvcmp2.cc,
src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test,
src/tgbatest/kv.test, src/tgbatest/ltl2neverclaim.test,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcounter.test,
src/tgbatest/ltlprod.cc, src/tgbatest/ltlprod.test,
src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test,
src/tgbatest/neverclaimread.test, src/tgbatest/nondet.test,
src/tgbatest/obligation.test, src/tgbatest/powerset.cc,
src/tgbatest/randpsl.test, src/tgbatest/randtgba.cc,
src/tgbatest/randtgba.test, src/tgbatest/readsave.test,
src/tgbatest/renault.test, src/tgbatest/scc.test,
src/tgbatest/sccsimpl.test, src/tgbatest/spotlbtt.test,
src/tgbatest/spotlbtt2.test, src/tgbatest/taatgba.cc,
src/tgbatest/taatgba.test, src/tgbatest/tgbaread.cc,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.cc,
src/tgbatest/tripprod.test, src/tgbatest/wdba.test,
src/tgbatest/wdba2.test, wrap/Makefile.am, wrap/python/Makefile.am,
wrap/python/ajax/Makefile.am, wrap/python/ajax/spot.in,
wrap/python/buddy.i, wrap/python/spot.i,
wrap/python/tests/Makefile.am, wrap/python/tests/alarm.py,
wrap/python/tests/bddnqueen.py, wrap/python/tests/implies.py,
wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltl2tgba.test, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py, wrap/python/tests/minato.py,
wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py,
wrap/python/tests/parsetgba.py, wrap/python/tests/run.in,
wrap/python/tests/setxor.py: Update licence version, and replace the
FSF address by a URL.

* src/tgba/bdddict.hh, src/tgba/bdddict.cc: Store variable types and
associated formula in a vector indexed by BDD variable numbers,
instead of using several maps.
* src/evtgbaalgos/tgba2evtgba.cc, src/tgba/bddprint.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/save.cc: Adjust usage.

* src/tgba/tgbaexplicit.hh: Rerganize a bit to
allow different functions to be used to format
states.  Add an enabled_utf8() method to
tgba_explicit_formula.
* src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc:
Simplify the interface by not depending on
dotty_decorator explicitely.
* src/tgba/bddprint.hh (enable_utf8): New function.
* src/tgba/bddprint.cc (enable_utf8): Implement it
and use the global utf8 flag in other functions.
* src/tgbatest/ltl2tgba.cc: Add an -8 option for
UTF-8 outpout.
* wrap/python/spot.i: Adjust for tgbexplicit.hh
changes.

* bench/Makefile.am, bench/gspn-ssp/Makefile.am,
bench/gspn-ssp/defs.in, bench/scc-stats/Makefile.am,
bench/split-product/Makefile.am, configure.ac,
iface/Makefile.am, iface/gspn/Makefile.am, iface/gspn/ssp.hh,
iface/nips/Makefile.am, iface/nips/common.cc,
iface/nips/common.hh, iface/nips/dottynips.cc,
iface/nips/nips.cc, iface/nips/nips.hh, src/Makefile.am,
src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
src/eltlparse/eltlscan.ll, src/eltlparse/fmterror.cc,
src/eltlparse/parsedecl.hh, src/eltltest/Makefile.am,
src/eltltest/defs.in, src/eltltest/nfa.cc, src/evtgba/evtgba.hh,
src/evtgba/product.cc, src/evtgba/product.hh,
src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaparse/Makefile.am,
src/evtgbaparse/evtgbaparse.yy, src/evtgbatest/defs.in,
src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
src/evtgbatest/readsave.test, src/ltlast/atomic_prop.cc,
src/ltlast/atomic_prop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlenv/environment.hh,
src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
src/ltltest/Makefile.am, src/ltltest/defs.in,
src/ltltest/equals.cc, src/ltltest/equals.test,
src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/ltltest/randltl.cc, src/ltltest/readltl.cc,
src/ltltest/reduccmp.test, src/ltltest/syntimpl.cc,
src/ltltest/syntimpl.test, src/ltltest/tostring.cc,
src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
src/ltltest/tunenoform.test, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/clone.hh,
src/ltlvisit/contain.cc, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/randomltl.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/misc/bddalloc.cc,
src/misc/bddop.cc, src/misc/bddop.hh, src/misc/freelist.hh,
src/misc/hash.hh, src/misc/minato.cc, src/misc/minato.hh,
src/misc/optionmap.cc, src/misc/timer.cc, src/misc/timer.hh,
src/saba/Makefile.am, src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/Makefile.am, src/sabatest/defs.in,
src/sanity/Makefile.am, src/tgba/Makefile.am,
src/tgba/bdddict.cc, src/tgba/bddprint.cc,
src/tgba/formula2bdd.cc, src/tgba/state.hh,
src/tgba/succiterconcrete.cc, src/tgba/taatgba.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbacomplement.cc,
src/tgba/tgbacomplement.hh, src/tgba/tgbaexplicit.cc,
src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc,
src/tgba/tgbaunion.hh, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/tgbaparse.yy, src/tgbatest/Makefile.am,
src/tgbatest/bddprod.test, src/tgbatest/complementation.cc,
src/tgbatest/complementation.test, src/tgbatest/defs.in,
src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
src/tgbatest/explpro3.test, src/tgbatest/explpro4.test,
src/tgbatest/explprod.cc, src/tgbatest/explprod.test,
src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.cc,
src/tgbatest/ltlprod.test, src/tgbatest/mixprod.cc,
src/tgbatest/mixprod.test, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/readsave.test,
src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
src/tgbatest/reductgba.test, src/tgbatest/taatgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.cc, src/tgbatest/tripprod.test,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py:
Fix copyrights.

* src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
Transform this static function into a member function.
* src/ltlvisit/destroy.hh (destroy): Document and declare as
deprecated.
* bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
src/ltlast/automatop.cc, src/ltlast/binop.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
src/ltltest/equals.cc, src/ltltest/randltl.cc,
src/ltltest/readltl.cc, src/ltltest/reduc.cc,
src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/bddprint.cc, src/tgba/taa.cc,
src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
the #include "destroy.hh" when appropriate.

Here are the reverted patches:
8c0d1003,
25a31142,
9afbaf63,
dc0005f4,
543190f2.

Merge all eltlast/ files into formula.hh (except automatop.hh).

src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlparse/fmterror.cc, src/ltlparse/public.hh,
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc,
src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd>
in headers, and prefer <ostream> in the body whenever possible.
* src/sanity/style.test, HACKING: Check and document this.

* src/sanity/Makefile.am (check-local): Run it.
* src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc,
src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc,
src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style
issues reported by style.test.

just strip the last one.  Escaping must be done at output.
* iface/gspn/gspm.cc (format_state): Likewise.
* src/misc/escape.hh, src/misc/escape.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgba/bddprint.cc (bdd_format_accset): New function.
* src/tgba/bddprint.hh (bdd_format_accset): New function.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state):
Escape the state name using escape_str().
(dotty_bfs::process_link): Escape conditions and acceptance
conditions using escape_str().
* src/tgbaalgos/save.cc (save_bfs::start): Call print_acc().
(save_bfs::print_acc): New function extracted from save_bfs::start().
Escape each acceptance condition.
(save_bfs::process_state): Use escape_str() and print_acc()

functions.
* src/tgba/bddprint.cc (bdd_print_accset): Declare it.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it.
* src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust
expected output.

arcs.  ltl2tgba_fm benefits from this and join multiple arcs with
the same destination and acceptance conditions.
* src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula,
bdd_format_formula): New functions.
* src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition,
tgba_explicit::add_condition, tgba_explicit::add_neg_condition,
tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition,
tgba_explicit::get_accepting_condition,
tgba_explicit::add_accepting_condition): Take a const formula*.
* src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition):
Rewrite using formula_to_bdd.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use
bdd_print_formula to display conditions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Likewise.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula):
New function.
(translate_dict::conj_bdd_to_atomic_props): Remove.
(ltl_to_tgba_fm): Factor successors on accepting conditions
and destinations, not conditions.  Use bdd_to_formula to translate
the conditions.
* src/tgbaparse/tgbaparse.yy: Expect conditions as a formula
in a string, call the LTL parser for this.
* src/tgbaparse/tgbascan.ll: Process " and \ escapes in
strings.
* src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust to new syntax for explicit
automata.

* Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
iface/gspn/Makefile.am, iface/gspn/common.cc,
iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/ltltest/Makefile.am,
src/ltltest/defs.in, src/ltltest/equals.cc,
src/ltltest/equals.test, src/ltltest/lunabbrev.test,
src/ltltest/nenoform.test, src/ltltest/parse.test,
src/ltltest/parseerr.test, src/ltltest/readltl.cc,
src/ltltest/tostring.cc, src/ltltest/tostring.test,
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.hh,
src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
src/tgba/succiterconcrete.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/save.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
src/tgbatest/bddprod.test, src/tgbatest/defs.in,
src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
wrap/python/spot.i, wrap/python/cgi/Makefile.am,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
wrap/python/tests/run.in: Add Copyright license.

dictionaries (map of BDD variables to LTL formulae).  This was
cumbersome, because to multiply two automata we had to build a
common dictionary (the union of the two LTL formula spaces), and
install wrappers to translate each automaton's BDD answers into
the common dictionary.  This translation, that had to be repeated
when several products were nested, was time consuming and was a
hindrance for some optimizations.
In the new scheme, all automata involved in a product must
share the same dictionary.  An empty dictionary should be
constructed by the user and passed to the automaton' constructors
as necessary.
This huge change removes most code than it adds.

* src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la.
* src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files.  These
partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc.
* src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc.
* src/tgba/bddfactory.hh, src/tgba/bddfactory.cc,
src/tgba/dictunion.hh, src/tgba/dictunion.cc,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.hh,
src/tgba/tgbabddtranslatefactory.cc,
src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc:
Delete.
* src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files.  These
replaces tgbabdddict.hh and tgbabdddict.cc, and also part of
bddfactory.hh and bddfactory.cc.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgba/succiterconcrete.cc (succ_iter_concrete::next()):
Get next_to_now from the dictionary.
* src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*,
not a const tgba_bdd_dict*.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh:
Adjust to use the new dictionary, stored in data_.
* src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh: Likewise.  Plus
now_to_next_ is now also stored in the dictionary.
* src/tgba/tgbabddconcreteproduct.cc: Likewise.  Now
that both operand share the same product, there is not
point in using tgba_bdd_translate_factory.
* src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh:
Store a bdd_dict (taken as constructor argument).
(tgba_bdd_core_data::~tgba_bdd_core_data): Remove.
(tgba_bdd_core_data::translate): Remove.
(tgba_bdd_core_data::next_to_now): Remove (now in dict).
(tgba_bdd_core_data::dict): New pointer.
* src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Adjust to use the new dictionary.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise.  Do
not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to
use bdd_dict* instead of tgba_bdd_dict&.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise.
(ltl_to_tgba): Take a dict argument.
* src/tgbaparse/public.hh (tgba_parse): Take a dict argument.
* src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate
a dictionary, and pass it to the automata' constructors.
* src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag)
option.
* iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument.
(tgba_gspn::get_dict): Adjust return type.
* iface/gspn/gspn.cc: Do not use bdd_factory, adjust to
use the new dictionary instead.

* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh.
(libtgbaalgos_la_SOURCES): Add lbtt.cc.
* src/tgba/bddprint.cc (print_sat_handler): Put a space after "!".
* src/tgbatest/readsave.test: Adjust spaces after "!".

of these accepting set so that they are really usable.  Provide
a all_accepting_conditions() method for use in the emptyness
check, and a neg_accepting_conditions() for products.
Predeclare TGBA accepting conditions is the i/o.

* src/tgba/bddprint.cc (want_prom): Rename as ...
(want_prom): ... this.
(print_handler): Adjust to display Acc[].
(print_acc_handler, bdd_print_acc): New functions.
* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
New functions.
* src/tgba/succiter.hh (current_promise): Rename as ...
(current_accepting_conditions): ... this.
* src/tgba/succiterconcrete.cc (current_state):
Rename next to now.
(current_promise): Rename as ...
(current_accepting_conditions): ... this, and compute
the accepting conditions.
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.cc,
src/tgbaalgos/dotty.cc: Adjust to new names.
* src/tgba/tgba.hh (all_accepting_conditions,
neg_accepting_conditions): New functions.
* src/tgba/tgbabddconcretefactory.cc: Adjust to new
names, and record accepting conditions instead of promises.
* src/tgba/tgbabddcoredata.hh (accepting_conditions,
all_accepting_conditions, negacc_set): New variables.
(notnow_set, notprom_set, declare_promise): Rename as ...
(notnext_set, notacc_set, declare_accepting_condition): ... these.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::current_promise): Rename as ...
(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
(tgba_explicit::add_promise): Rename as ...
(tgba_explicit::add_accepting_condition): ... this.
(tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition): New variables.
(tgba_explicit::get_promise): Rename as ...
(tgba_explicit::get_accepting_condition): ... this.
(tgba_explicit::all_accepting_conditions,
tgba_explicit::neg_accepting_conditions): Implement them.
(all_accepting_conditions, neg_accepting_conditions,
all_accepting_conditions): New variables.
(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
* src/tgba/tgbaexplicit.cc: Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
(tgba_product::all_accepting_conditions,
tgba_product::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.hh:
(tgba_translate_proxy::all_accepting_conditions,
tgba_translate_proxy::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.cc: Likewise.
* src/tgbaalgos/save.cc (save_rec): Call bdd_print
(tgba_save_reachable): Output the `acc =' line.
* src/tgbaparse/tgbaparse.yy: Support the for
accepting conditions definitions using an "acc =" line
at the start.  Later, use has_accepting_condition while
parsing	accepting conditions to ensure they were declared.
Disallow !cond in accepting conditions.
* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
* src/tgbatest/explicit.cc (main): Declare accepting conditions.
* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
and -R new options.
* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
recent changes.

when !want_prom.
* src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or
identifiers.  Discard empty strings.
* src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod.
(mixprod_SOURCES): New variable.
(TESTS): Add mixprod.test.

src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include <cassert>.

(want_prom): New global static variable.
(print_handle): Honor want_prom.
(print_sat_handler, bdd_print_sat, bdd_format_sat): New functions.
(bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom.
* src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions.
* src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add
save.cc and save.hh.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave.
(readsave_SOURCES): New variable.
(TESTS): Add readsave.test.

src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc:
Add Doxygen comments.

* src/tgba/bddprint.cc (bdd_format_set): Likewise.
* src/tgba/state.hh: Add Doxygen comments.
(state::compare): Take a state*, not a state&.
(state_ptr_less_than): New functor.
* src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a
state&.
* src/tgba/statebdd.cc (state_bdd::compare): Likewise.
* src/tgba/succiter.hh: Add Doxygen comments.
* src/tgba/tgba.hh: Mention promises.
(tgba::formate_state): New pure virtual method.
* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state):
New method.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state):
Likewise.
* src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than
and tgba::formate_state.

* src/tgba/Makefile.am (libtgba_la_SOURCES): Add them.
* src/tgba/public.hh: Include bddprint.hh.