intricate memory corruption bug prevented me to check the patch
in. It took me two days to realize why find_state() must do a
double loop over the candidates to check for equality before
checking for inclusion(s).
* iface/gspn/ltlgspn.cc: New options, -e45 and -n.
* iface/gspn/ssp.cc, iface/gspn/ssp.hh: Handle these.
* src/tgbaalgos/gtec/gtec.cc (TRACE): Add some debugging traces.
(couvreur99_check_shy::dump_queue): New function.
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::dump_queue):
New function.
(couvreur99_check_shy_ssp): Add a onepass_ attribute to
disable the "shyness", and do not increment pos before calling
find_state since gspn's implementation uses it.
* iface/gspn/ssp.cc: Enable "onepass_" for all "shy" variants,
and also fix find_state for the case where onepass_ is
disabled (but I do not yet know why the latter fix isn't enough).
numbered_state_heap_ssp_semi): Implement a double hash_map using
greatspn's new container() function.
* iface/gspn/ssp.hh (gspn_ssp_interface): Add a doublehash option.
* iface/gspn/ltlgspn.cc: Add option -1 to disable this optimization.
Reorganize this function so that syntactically there is only one
loop over the successors, and not two. Call reintroduce the call
to couvreur99_check_shy::state_index(), needed by SSP, and
suppress that to index_and_insert introduced on 2004-12-29. Also
split the "group" option in two: "group" and "group2". "group2"
is the equivalent of the older "group", while the new "group" is
weaker and faster.
(couvreur99_check_shy::state_index): Change prototype as needed by
the algorithm.
* src/tgbaalgos/gtec/gtec.hh: Adjust.
* src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc
(index_and_insert): Remove.
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust
to new prototype.
* bench/emptchk/README, bench/emptchk/algorithms: Adjust references
to group/group2.
option_map::set): Handle default values.
(anonymous::to_int): Do not print anything.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in
the constructor.
* src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise. Handle
the "poprem", "group", and "shy" options via the option_map.
Supply a couvreur99() wrapper to the shy/non-shy variant.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
iface/gspn/ssp.cc: Adjust.
(index_and_insert): New function.
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): Rewrite.
(couvreur99_check_shy::clear_todo): New method.
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::todo_item): New
struct.
* iface/gspn/ssp.cc (numbered_state_heap_ssp_semi::index_and_insert):
New method.
so it doesn't have to compute it.
* src/tgbaparse/tgbascan.ll: Likewise.
(YY_USER_INIT, current_file): Remove, it is too costly to use
yy::Location::filename in the current implementation
of yy::Location (this attribute is duplicated for each token).
Leaving it empty divides the parsing time by 3.
* src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh
(format_tgba_parse_errors): Take the filename as argument.
* src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls
to format_tgba_parse_errors.
(couvreur99_check_status::cycle_seed): New attribute.
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check,
couvreur99_check_shy::check): Fill cycle_seed.
* src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc:
(couvreur99_check_result::accepting_run,
couvreur99_check_result::accepting_cycle): Revamp to compute a
cycle from the cycle_start, and then the shortest prefix to this
cycle.
(couvreur99_check_shy::couvreur99_check_shy): Add the group option,
and redefine todo as a list so it can be iterated over.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce
couvreur99_shy- (for group=false) in addition to couvreur99_shy
(for group=true).
* iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi,
couvreur99_check_ssp_shy): Use group=true;
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh,
src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen
groups in the documentation. Presently this only covers the
tgba/ directory, and the emptiness-check algorithms.
* doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files
in src/evtgbaparse/.
src/tgbaalgos/magic.cc, call explicit_magic_search() instead of
building a spot::magic_search.
* iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run().
src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba*
argument before the tgba_run* argument (for consistency with
replay_tgba_run).
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust
calls to print_tgba_run().
algorithms to conform to it, uniformly. This will unfortunately
break third-party code that were using these algorithms.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
* src/tgbaalgos/Makefile.am: New files.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
conform to the new emptiness-check interface.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Likewise. The classes have been renamed are as following
emptiness_check -> couvreur99_check
emptiness_check_shy -> couvreur99_check_shy
counter_example -> couvreur99_check_result
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
iface/gspn/ssp.cc: Adjust to renaming and new interface.
class gspn_environment, and move it to ...
* src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file
as class declarative_environment.
* src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh.
(libltlenv_la_SOURCES): Add declenv.cc.
* iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc,
iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references
to declarative_environment.
the `inclusion' flag.
* iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call
inclusion_version when inclusion is set.
* iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3,
-e4, and -e5.
and dead_prop from the dead argument passed to the constructor.
(tgba_succ_iterator_gspn): Stutter on dead transitions.
(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
dead argument.
* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
dead property.
* iface/gspn/udcseltl.test: Try option -d.
* 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.
