two unabbreviate_logic definitions (const and non-const) into a
function that takes a const formula* and return a non-const
formula*.  Since formula* is convertible to const formula*, and
the const version of the function just called the non-onst one, it
makes no sense to keep both.  Also, it confused Swig.
* src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Likewise
for negative_normal_form.
* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: Likewise
for unabbreviate_ltl.
* src/ltlvisit/clone.cc, src/ltlvisit/clone.hh: Likewise for clone.
* src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh: Likewise
for destroy.

* src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh.

* iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition
WITH_GSPN.

(ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES)
(ltlgspn_srg_SOURCES): New variables.
(check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg.

* iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install
gspn.hh.

(tgba::project_state): New method.
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product::project_state): New method.
* src/tgba/tgbabta.hh, src/tgba/tgbabta.cc
(tgba_bta_proxy::project_state): New method.
* src/tgbaalgos/magic.cc (magic_search::print_result): Take
a restrict argument.

* src/ltltest/parse.test: Test them.

(tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables.
* src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally.
* src/tgbatest/spotlbtt.test: Include tbalbtt in the tests.

(tgba_tba_proxy::state_is_accepting): New method.
* src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
tgbaalgos_HEADERS): Add them.
* src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files.
* src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES,
check_PROGRAMS): Add them.

* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh.
(libtgba_la_SOURCES): Add tgbatba.cc.
* src/tgbatest/ltl2tgba.cc: Add option -D.

* src/misc/bddlt.hh: ... in this new file.
* src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh.

(libtgbaalgos_la_SOURCES): Add reachiters.cc.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using
spot::tgba_reachable_iterator_breadth_first.
* src/tgbatest/explicit.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust expected output.

the root of a product to reduce its number of successors.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc.
* src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and
global_automaton arguments.
(tgba::support_conditions, tgba::support_variables,
tgba::compute_support_conditions, tgba::compute_support_variables):
New functions.
(tgba::last_support_conditions_input_,
tgba::last_support_conditions_output_,
tgba::last_support_variables_input_,
tgba::last_support_variables_output_): New attributes.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter):
Handle the two new arguments.
(tgba_bdd_concrete::compute_support_conditions,
tgba_bdd_concrete::compute_support_variables): Implement them.
* src/tgba/tgbabddconcrete.hh: Adjust.
* src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter):	Ignore
the two new arguments.
(tgba_explicit::compute_support_conditions,
tgba_explicit::compute_support_variables): Implement them.
* src/tgba/tgbaexplicit.hh: Adjust.
* src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the
two new arguments.
(tgba_product::compute_support_conditions,
tgba_product::compute_support_variables): Implement them.
* src/tgba/tgbaproduct.hh: Adjust.
* iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input,
tgba_gspn_private_::last_state_cond_output,
(tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input.
(tgba_gspn_private_::~tgba_gspn_private_): Delete
last_state_cond_input.
(tgba_gspn_private_::state_conds): New function, eved out
from tgba_gspn::succ_iter.
(tgba_gspn::succ_iter): Use it.  Use the two new arguments.
(tgba_gspn::compute_support_conditions,
tgba_gspn::compute_support_variables): New functions.
* iface/gspn/gspn.hh: Adjust.

Disallow copy for security.

* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
* src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
* src/tgba/tgbabddconcreteproduct.cc
(tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory,
product): Take operand automata as pointers.
* src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
(tgba_product): Disallow copy.
(tgba_product::tgba_product): Take operand automata as pointers.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
Take tgba arguments as pointer.
* src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
* src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
* src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
Likewise.
* src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
* src/tgbaalgos/save.hh (save): Likewise.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.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: Likewise.

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.

Forward root_ to children of And.
(ltl_trad_visitor::recurse): Take a root argument.

(tgba_bdd_concrete_factory::add_relation): Rename as ...
(tgba_bdd_concrete_factory::constrain_relation): ... this.
* src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc:
Adjust.

not create Now/Next variable when G is the root of the formula.
(ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
(ltl_trad_visitor::recurse): Create a new visitor, do not copy
the current one.
(ltl_to_tgba): Build ltl_trad_visitor with root = true.

* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
Remove FIXME about handling X(a U b) and X(a R b) better, it's
done naturally.

Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f]
is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]),
not !Acc[g].Acc[f] + p.Acc[g].!Acc[f].

* Makefile.am (MAYBE_LBTT): New variables.
(SUBDIRS): Add $(MAYBE_LBTT).
(EXTRA_DIST): Add m4/lbtt.m4.
* configure.ac: Call AX_CHECK_LBTT.
* m4/lbtt.m4: New file.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt.
(spotlbtt_SOURCES): New variables.
(TESTS): Add spotlbtt.test.
(CLEANFILE): Add config.
* src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New
substitutions.
* src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files.

Fix computation of states sharing the same accepting state.

* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
to designate initial states.
(lbtt_reachable): Adjust calls to fill_todo.  Handle the
fake initial state accepting conditions specially.
* src/tgbaalgos/lbtt.hh: Update comments.

guards with -1 in output.

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

current_accepting_conditions): Mark as const.
* src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh:
Likewise.

(tgba_succ_iterator_concrete::current_acc_): New attribute.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Set current_acc_.
(tgba_succ_iterator_concrete::current_accepting_conditions):
Simply return it.

tgba_bdd_core_data::translate): Handle all_accepting_conditions.
* src/tgba/tgbabddconcretefactory.cc
(tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions.

accepting conditions w.r.t. to Now variables, not Next.

Simplify, do not call next_non_false_() either side is done.

State that this is a boolean function.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): Remove.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
tgba_succ_iterator_concrete::first): Adjust to removed members.
(tgba_succ_iterator_concrete::next): Simplify, transitions
are no labelled by boolean functions, not only conjunctions.
Suggested by Denis Poitrenaud.

function.
* src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate):
Likewise.
* src/tgba/tgbabddtranslatefactory.cc
(tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use
tgba_bdd_core_data::translate.

New attribute.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
Handle nownext_set.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Use nownext_set to simplify.