the same node twice when dealing with loops.

* src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix.
(minato_isop::next): Avoid useless intermediate variables.
* src/misc/minato.hh: Typo in comments.

Introduce bdd_satprefix, to speedup spot::minato().

* src/bdd.h (bdd_satprefix): New function.
* src/bddop.c (bdd_satprefix, bdd_sat_prefixrec): New functions.

If the input is a tgba_explicit_formula we can output a
tgba_explicit_formula too, and we want to do that because it is
more space efficient.

* src/tgba/tgbaexplicit.hh (get_label): New method.
* src/tgbaalgos/sccfilter.cc (create_transition): New function,
to handle tgba_explicit_formula and tgba_explicit_string output
differently.
(filter_iter): Template it on the output tgba type, and adjust
to call create_transition.
(scc_filter): Use filter_iter<tgba_explicit_formula> or
filter_iter<tgba_explicit_string> depending on the input tgba
type.

A useless acceptance conditions is one that is always implied by
another.

* src/misc/bddop.hh, src/misc/bddop.cc
(compute_neg_acceptance_conditions): New function.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(set_acceptance_conditions): New function.
* src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
Keep track of useful acceptance conditions.
(useful_acc_of): New function.
* src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
attributes.
* src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
useless acceptance conditions.
(scc_filter): Compute useful acceptance conditions and pass them
to filter_iter.

after removing acceptance conditions.

* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh (prune_scc,
prune_acc, remove_component, compute_scc, remove_acc,
is_not_accepting, delete_scc, is_terminal, remove_scc,
display_scc): Remove anything related to the simplification of
SCCs.

prune_scc() leaked memory and failed to remove chains of useless SCCs.

* src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call
scc_filter() instead of prune_scc(), and do it before running
any simulation-based reduction.
* src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const
tgba*.
* src/tgbatest/ltl2tgba.cc: Call scc_filter() instead of
prune_scc().
* src/tgbatest/scc.test: Add two more tests that failed with
prune_scc().

* src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: New
files.
* src/tgbaalgos/Makefile.am: Add them.

Also compute useless SCCs.

* src/tgbaalgos/scc.cc (scc_map::scc::trivial): New field.
(scc_stats::useless_scc_map): New field.
* src/tgbaalgos/scc.cc (scc_map::build_map): Mark SCCs that are
not trivial.
(scc_map::accepting): Always return false for trivial SCC.
(build_scc_stats): Fill in useless_scc_map.

* src/tgbaalgos/reachiter.hh (tgba_reachable_iterator::want_state):
New method.
* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::want_state):
Implement it.
(tgba_reachable_iterator::run): Call want_state before processing
a state.

of by pointer.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Fix copyright
header.

counter updated each time we create a new (unique) formula.

Doing so saves a lot of memory during the translation of the
ltlcounter formulae, because the formulae are quite big and
storing a string representation of each formula on its node was a
bad idea.  For instance with n=12, the translation now uses 40MB
where it used 290MB.  (Note: in both cases, 20MB is being used by
the BDD cache.)

* src/ltlast/formula.hh (hash_key_): Rename as ...
(count_): ... this.
(hash): Adjust.
(max_count): New static variable to count the number of
formulae created.
(formula): Update max_count and set count_.
(dump): Make it a virtual pure method.
(set_key_): Remove.
(formula_ptr_less_than): Speed up and return false when
the two formula pointer are equal.
* src/ltlast/formula.cc (set_key_, dump): Remove.
* 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/constant.cc,
src/ltlast/constant.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
Empty the constructor (do not precompute the dump_ anymore),
and add a dump() implementation.

* bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations.
* src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/spotlbtt.test: Likewise.

* src/tgbatest/ltl2tgba.cc (syntax): Reorganize the help text, so
that we can find options without resorting to grep...  Also
cleanup the program name if it is a libtool wrapper.

translation.  It still is the default translation.
(opt_fm, opt_taa): Replace these two variables by ...
(translation): ... this enum.  And use a switch to call the
correct translation.

* wrap/python/spot.i: Do not include clone.hh and destroy.hh.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix a typo
introduced three patches ago in the handling of unobserved events.

much time when the formula is large, and it is useless when the
purpose is model-checking with Spin.

* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the
comments option.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs,
never_claim_reachable): Honor the comment option.
* src/tgba/tests/ltl2tgba.cc (-N): Do not comment states.
(-NN) New option to output a commented never claim.

* src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both
the translation and the language containment checker.
* src/tgbatest/spotlbtt.test: Update TAA related tests.

This gives a nice speedup (>1.4) in the ltlcounter benchmark,
because we no longer have to generate a copy the string
representations of the LTL formulae.

* src/tgbaalgos/ltl2tgba_fm.cc: Adjust.  Also get rid of the
formulae_seen map, since we can now ask the tgba_explicit_formula
if it knows the state.

* src/tgbatest/ltl2tgba.cc: Dump all LTLinstances with their
reference count.

tgba_explicit instances labelled by other objects than strings.

* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Split tgba_explicit in two levels: tgba_explicit with unlabelled
states, and tgba_explicit_labelled templated by the type of
the label.  Define tgba_explicit_string (with the interface
of the former tgba_explicit class) and tgba_explicit_formula
for future use in ltl2tgba.cc.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
use tgba_explicit_string when appropriate.

* m4/boost.m4: Rewrite like I already did in Vaucanson.

the test case might become too slow for the autobuilder.

* bench/ltlcounter/README, bench/ltlcounter/run,
bench/ltlcounter/plot.gnu, bench/ltlcounter/defs.in,
bench/ltlcounter/Makefile.am: New files.
* bench/Makefile.am (SUBDIRS): Add ltlcounter.
* configure.ac (AC_CONFIG_FILES): Adjust.
* THANKS: Add her.

* src/tgbatest/ltl2tgba.cc: Add option -T.

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

* src/ltlvisit/clone.hh (clone): Document and declare as deprecated.
* src/ltlast/formula_tree.cc, src/ltlvisit/basicreduce.cc,
src/ltlvisit/clone.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcretefactory.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbatest/complementation.cc, wrap/python/tests/ltlsimple.py:
Adjust clone() usage, and remove the #include "clone.hh" when
appropriate.

* src/ltlast/formula.hh, src/ltlast/formula.cc (clone): Declare
as const.

and formula::destroy.

* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/formula.hh, src/ltlast/formula.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/destroy.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/reduce.cc,
src/tgbatest/randtgba.cc: Adjust.

Before this patch, every time you cloned a formula, the clone
visitor would recurse into the entire AST to increment the
reference count of all nodes.  When running ltl2tgba_fm on
the formula generated by "LTLcounterLinear.pl 8", approx 27% of
the time was spent in the clone visitor.

After this patch, cloning a formula is just an increment of the
reference count of the top node.  Children are decremented only
when the top node's ref count is decremented to zero.  With this
change, clone() and destroy() become constant time, the
ltl2tgba_fm spend only 0.01% of the time cloning formulae.

* src/ltlast/automatop.cc (~automatop): Decrement children.
(instance): Decrement children if the instance already exists.
* src/ltlast/binop.cc, src/ltlast/multop.cc, src/ltlast/unop.cc:
Likewise.
* src/ltlvisit/clone.cc (clone): Simplify, now we only need to
call ref().
* src/ltlvisit/destroy.cc (destroy): Simplify, now we only need
to call unref().
(destroy_visitor): Remove, no longer needed.

* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh:
Add a dump_instance() static method to all class.
* src/ltltest/readltl.cc: Add option -r to dump all instances
with their reference count, after parsing and after deletion.

* src/ltlast/unop.hh (map): Use unop* as values.
* src/ltlast/binop.hh (map): Use binop* as values.
* src/ltlast/multop.hh (map): Use multop* as values.
* src/ltlast/automatop.hh (paircmp): Rename as tripletcmp.
(map): Use automaton* as values, not formula*.

* src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing
instance_count() functions.
* src/tgbatests/eltl2tgba.cc: Add missing instance_count()
assertions at the end.
* src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(),
even if automatop are not used in ltl2tgba yet.  This way we won't
forget once eltl2tgba and ltl2tgba are merged.

in taa_succ_iterator and allow multiple initial states in taa.
* src/tgba/ltl2taa.cc: Remove temporary printing.

* src/tgbatest/defs.in (srcdir): Adjust from VPATH builds.
* src/tgbatest/ltlcounter.test (lcdir): Adjust definition to
new value of $srcdir.
(run): Fix setting of $run after $n = 2.  Using run=: would in
fact disable all the big tests...

formulae (i.e. n<=2) under valgrind.  The test case is too
slow otherwise.

* src/sanity/style.test: Make sure sh does not abort when read
exits with false.