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.
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.
* 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.
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.
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):
into ...
(emptiness_check_shy): This new subclass of emptiness_check.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.
* 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;
