version a separate variable.

never_claim_reachable, and cgi.escape its output.
Lighten the color a bit.

src/tgba/bddprint.hh: Fix Doxygen comments.

arguments.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
New method.
(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
Use it.

the new variable dot_bgcolor.

using this new function.

* wrap/python/cgi/ltl2tgba.in: Display the never claim on demand.

Convert a formula into a string parsable by Spin.
* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files.
Print the never claim in Spin format of a degeneralized TGBA.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the
never claim in Spin format of a degeneralized TGBA.
* src/tgbatest/ltl2neverclaim.test: New file.
* src/tgbatest/Makefile.am: Add it.

when valgrind is not used.
Reported by Denis Poitrenaud.

* src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document
it.
Reported by Denis Poitrenaud.

counter-example computation for -e5 too.

(main) [SSP]: Use the standard counter-example computation
for -e and -e1.

* iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
iface/gspn/dottyeesrg.cc: Rename as ...
* iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc:
... these.  Adjust all classes and function names.
* iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes
filenames and function names.
* m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS.

Rewrite.
(numbered_state_heap_hash_map::index): New functions.
(numbered_state_heap_hash_map::filter): Delete.
* src/tgbaalgos/gtec/nsheap.hh
(numbered_state_heap_hash_map::index): New functions.
(numbered_state_heap_hash_map::filter): Delete.
* iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find,
numbered_state_heap_eesrg_semi::index): Rewrite.
(numbered_state_heap_eesrg_semi::filter): Remove.
* src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc:
Adjust to use find() and index() instead of filter()..

Free filtered states.
(emptiness_check_shy_eesrg): New class.
(emptiness_check_eesrg_shy): New function.
* iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
* iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
* * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
(emptiness_check_shy::check): Move arc, num, succ_queue, and todo
as attributes.
(emptiness_check_shy::find_state): New virtual function.

connected_component_eesrg_factory, numbered_state_heap_eesrg_semi,
numbered_state_heap_eesrg_const_iterator,
numbered_state_heap_eesrg_factory_semi): New classes.
(emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi,
counter_example_eesrg): New functions.
* iface/gspn/eesrg.hh (emptiness_check_eesrg_semi,
emptiness_check_eesrg_shy_semi, counter_example_eesrg): New
functions.
* iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.

state_gspn_eesrg): Compute the array of all successors of the
right state beforehand, pass it to Greatspn (left automata) at
once, let it compute the resulting synchronized arcs, and iterate
on that result.

numbered_state_heap_hash_map_factory): New class.
* src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory):
Implement it.
* src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check,
emptiness_check_shy::emptiness_check_shy): Take a
numbered_state_heap_factory argument.
* tgbaalgos/gtec/status.hh
(emptiness_check_status::emptiness_check_status): Likewise.
(emptiness_check_status::h): Make it a numbered_state_heap*.
* src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc,
tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h.

Delete and split into ...
* 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: ...
these new files.
* src/tgbaalgos/gtec/Makefile.am: New file.
* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
Recurse into gtec and link gtec/libgtec.la.
(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
and emptinesscheck.cc.
* configure.ac: Output src/tgbalagos/gtec/Makefile.
* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
* README: Update tree description.

numbered_state_heap, numbered_state_heap_hash_map): New classes.
* tgbaalgos/emptinesscheck.cc
(numbered_state_heap_hash_map_const_iterator): New class.
(numbered_state_heap_hash_map): Implement it.

(explicit_connected_component_factory,
connected_component_hash_set_factory): New classes.
(counter_example::counter_example): Take an
explicit_connected_component_factory factory argument.
* src/tgbaalgos/emptinesscheck.cc: Adjust.

New class.
(counter_example::connected_component_set): Rename as ...
(connected_component_hash_set): ... this, and inherit from
explicit_connected_component.
(counter_example::accepting_path, counter_example::complete_cycle):

(counter_example::connected_component_set::has_state): Return
a const state* and behave like h_filt.
* src/tgbaalgos/emptinesscheck.cc: Adjust.

into ...
(emptiness_check_shy): This new subclass of emptiness_check.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.

extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.

($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c.

extracted from ...
(emptiness_check): ... here.
* src/tgbaalgos/emptinesscheck.cc: Adjust.

from ...
(emptiness_check): ... here.
(emptiness_check::root): Redefined as a scc_stack object.
* src/tgbaalgos/emptinesscheck.cc: Adjust.

Do not visit a state more than once.  Report from Soheib Baarir.

variables from a shared bdd_dict.  Register Next variables as
anonymous variables.
(translate_dict::translate_dict, translate_dict::~translate_dict,
translate_dict::register_proposition,
translate_dict::register_a_variable,
translate_dict::register_next_variable,
translate_dict::dump, translate_dict::var_to_formula,
ltl_to_tgba_fm): Adjust.
(translate_dict::dict): New attribute.
(translate_dict::a_map, translate_dict::a_formula_map,
translate_dict::var_map, translate_dict::var_formula_map): Delete.

invalidated iterators.
* tgba/bdddict.cc (unregister_variable): New methods,
extracted from ...
(bdd_dict::unregister_all_my_variables): ... here.
* tgba/bdddict.hh (unregister_variable): Declare them.

methods.
* src/misc/freelist.cc (free_list::register_n,
free_list::releases_n): Rewrite using free_list::remove and
free_list::insert.
(free_list::remove, free_list::insert): New methods.
* src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables):
New method.
(bdd_dict::annon_free_list): New subclass.
(bdd_dict::free_annonymous_list_of_type_of): New attribute.
* src/tgba/bdddict.cc (bdd_dict::register_all_variables_of,
bdd_dict::unregister_all_my_variables): Handle anonymous variables
too.
(bdd_dict::register_anonymous_variables,
bdd_dict::annon_free_list::annon_free_list,
bdd_dict::annon_free_list::extend): New methods.

Fix handling of PATH when backtracking.  Report from Soheib Baarir.

* src/misc/freelist.hh, src/misc/freelist.cc: New files.
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
* src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
make dump_free_list visible.
* src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
all the code into free_list::register_n() and
bdd_allocator::extend(), and call the former.
(bdd_allocator::release_variables): Move all the code into
free_list::release_n() and call it.
(bdd_allocator::extend): New method.
* src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;

it is automatically distributed.
(EXTRA_lbtt_translate_SOURCES): Likewise, remove NeverClaim-parse.h.

* src/Makefile.am (AM_YFLAGS): ... do it here.
(BUILT_SOURCES): New variable.

blindly enumerate all combinations of atomic properties; initially
set all_props to the set of all possibly satisfiable combinations.