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/.
functionality of the old tgba_tba_proxy.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
each state, skipping the `bddtrue' stage now used only in
tgba_sba_proxy. Doing so removes approximately 6% of states in
the degeneralized tests of spotlbtt.test.
(tgba_sba_proxy): Implement it.
* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
to take a tgba_sba_proxy.
* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
never_claim_reachable().
check, degeneralize the automaton only if it has too much
acceptance conditions. This makes it easier to reproduce runs
of randtgba.
* src/tgbatest/emptchk.test: Adjust.
* src/tgbaalgos/se05.cc: Add a bit state hashing version.
* src/tgbaalgos/magic.hh: Make them public.
* src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks.
* src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test.
* src/tgbatest/dfs.test: Introduce new characteristic explicit tests.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS)
(libtgbaalgos_la_SOURCES): Add them.
* src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public.
* src/tgbatest/randtgba.cc: New file.
* src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it.
* src/tgbatest/readsave.test: Check a random graph.
src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
option to decide whether the output should look like that of
print_tgba_run() or a complete debug trace.
* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
debug=true.
prepare it to a bit state hashing version.
* src/tgbaalgos/magic.hh: adapt to the new interface of
magic_search and se05_search.
* src/tgbaalgos/se05.cc: new file.
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
* src/tgbatest/emptchk.test: more tests.
* src/tgbatest/dfs.test: new file.
* src/tgbatest/Makefile.am: Add it.
Rewrite as ...
(couvreur99_check_result::accepting_cycle): ... this less complex
implementation.
(couvreur99_check_result::complete_cycle): Delete.
* src/tgbatest/emptchke.test: More explicit examples.
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
as third parameter.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
dotty_bfs::process_link): Use the decorator.
* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
is given.
* src/tgbatest/emptchk.test: Exercize -g.
(tgba_reachable_iterator::process_link): Take the state* as arguments
in addition to the state numbers.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(tgba_explicit::copy_acceptance_conditions_of): New method.
* tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call
copy_acceptance_conditions_of.
(dupexp_iter::process_state, duplex_iter::declare_state,
dupexp_iter::name_): Remove.
(dupexp_iter::process_link): Adjust prototype, and format
the state here rather than in process_state.
* tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype
of process_link.
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().
tgba_succ_iterator) with some string. This comes handy to
associate that transition to its high-level name.
* src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation):
New method.
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
(tgba_product::transition_annotation): Implement it.
* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
(tgba_tba_proxy::transition_annotation): Likewise.
* src/tgbaalgos/replayrun.cc (print_annotation): New function.
(replay_tgba_run): Use it.
couvreur99_check_result::complete_cycle,
couvreur99_check_result::accepting_path): Record conditions and
acceptance conditions in the accepting run. Simplify the
todo BFS stack for accepting_run and complete_cycle.
* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
now everything works.
* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
when an outgoing transition is not found.
Cannot test them because the run returned by the emptiness checks
are currently incomplete (they lack the acceptance conditions, and
sometimes even the labels in the prefix).
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
when the emptiness checks are fixed.
