formula automaton and the synchronized product) from LBTT.
Idea from Jean-Michel Couvreur.
* src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
(nonacceptant_lbtt_reachable): New function.
* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
function.
* src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
if the -T option is used.
* src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
default.
* wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler)
(reset_alarm): New functions. Kill the script and its
children if it runs for too long.
(render_dot): Call reset_alarm.
* wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh.
* wrap/python/tests/minato.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add minato.py.
corresponding automaton via the automaton() method of the
gspn_interface and gspn_eesrg_interface classes.
* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take dict and
env arguments.
(gspn_interface::automaton): New method.
(tgba_gspn): Move all the declaration ...
* iface/gspn/gspn.cc (tgba_gspn): ... here.
(gspn_interface::automaton): Implement it.
* iface/gspn/eesrg.hh (gspn_eesrg_interface::gspn_eesrg_interface):
Take dict and env arguments.
(gspn_eesrg_interface::automaton): New method.
(tgba_gspn_eesrg): Move all the declaration ...
* iface/gspn/gspn.cc (tgba_gspn_eesrg): ... here.
(gspn_eesrg_interface::automaton): Implement it.
* iface/gspn/dottygspn.cc, iface/gspn/dottyeesrg.cc,
iface/gspn/ltlgspn.cc: Adjust.
Do not treat true and false specially. Otherwise it breaks
translation of F(false).
* src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not
use true as acceptance condition.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor): Use Acc[b] as
acceptance condition for Fb, not Acc[Fb].
After this change, degeneralized automata are 40% smaller
in LBTT's statistics.
* src/tgba/tgbatba.cc (state_tba_proxy): Store an iterator,
pointing somewhere into the acceptance conditions list, instead of
an acceptance condition.
(state_tba_proxy::acceptance_iterator): New method.
(tgba_tba_proxy_succ_iterator): Adjust to use iterators too.
(tgba_tba_proxy_succ_iterator::current_state): If the current
transition is in several consecutive acceptance steps after the
expected one, advance many steps at once.
(tgba_tba_proxy::tgba_tba_proxy): Build the acceptance cycle
as a list, not a map.
(tgba_tba_proxy::get_init_state, tgba_tba_proxy::succ_iter):
Adjust.
* src/tgba/tgbatba.hh (tgba_tba_proxy::acc_cycle_): Declare as
a list, not a map.
with same destination and acceptance conditions directly, without
calling a->merge_transition(). If one transitions goes to "True",
subtract its conditions from all other transitions; this optimizes
a U b.
* src/ltlast/refformula.cc (ref_formula::ref_count_): New method.
* src/ltlast/atomic_prop.hh (atomic_prop::dump_instance): New method.
* src/ltlast/atomic_prop.cc (atomic_prop::dump_instance): New method.
library for eesrg. Define the WITH_GSPN_EESRG conditional.
* iface/gspn/Makefile.am (gspn_HEADERS, check_PROGRAMS): Add the
eesrg items in condition WITH_GSPN_EESRG.
(libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS)
(libspotgspneesrg_la_SOURCES): Define only in condition
WITH_GSPN_EESRG.
just strip the last one. Escaping must be done at output.
* iface/gspn/gspm.cc (format_state): Likewise.
* src/misc/escape.hh, src/misc/escape.cc: New files.
* src/misc/Makefile.am: Add them.
* src/tgba/bddprint.cc (bdd_format_accset): New function.
* src/tgba/bddprint.hh (bdd_format_accset): New function.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state):
Escape the state name using escape_str().
(dotty_bfs::process_link): Escape conditions and acceptance
conditions using escape_str().
* src/tgbaalgos/save.cc (save_bfs::start): Call print_acc().
(save_bfs::print_acc): New function extracted from save_bfs::start().
Escape each acceptance condition.
(save_bfs::process_state): Use escape_str() and print_acc()
(to_string_visitor::visit(const atomic_prop*)): Quote propositions
that start with F, G, or X.
* src/ltltest/tostring.test: Test quoted propositions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Escape " and + characters in formulae.
* src/tgbatest/readsave.test: Test for this.
