* wrap/python/tests/run.in, iface/nips/nipstest/defs.in,
iface/gspn/defs.in: Do not disable VERBOSE when running from "make
check". Since we have started using parallel-check on 2009-08-31,
we should always send verbose output to the log.
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.
