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.
Use $(FROM_LTLPARSE_YY_MAIN), not $@, because $@ can contains
VPATH and we do not want Bison to see absolute paths.
* src/tgbaparse/Makefile.am ($(FROM_TGBAPARSE_YY_MAIN)): Likewise.
* src/ltlparse/ltlparse.yy: Simplify error handling now that Bison
will call destructors. Give each operator a full name, so that
Bison uses it in error messages.
(tgba_explicit::merge_transitions): New method.
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Factorize all
variables (not just Next and A) when computing prime implicants,
and then call merge_transitions().
(condition): ... this. We now accept only one condition, which
is a formula.
* src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition,
tgba_explicit::get_condition): Remove, unused.
* src/tgba/tgbaexplicit.cc: Likewise.
arcs. ltl2tgba_fm benefits from this and join multiple arcs with
the same destination and acceptance conditions.
* src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them.
* src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula,
bdd_format_formula): New functions.
* src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition,
tgba_explicit::add_condition, tgba_explicit::add_neg_condition,
tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition,
tgba_explicit::get_accepting_condition,
tgba_explicit::add_accepting_condition): Take a const formula*.
* src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition):
Rewrite using formula_to_bdd.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use
bdd_print_formula to display conditions.
* src/tgbaalgos/save.cc (save_bfs::process_state): Likewise.
* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula):
New function.
(translate_dict::conj_bdd_to_atomic_props): Remove.
(ltl_to_tgba_fm): Factor successors on accepting conditions
and destinations, not conditions. Use bdd_to_formula to translate
the conditions.
* src/tgbaparse/tgbaparse.yy: Expect conditions as a formula
in a string, call the LTL parser for this.
* src/tgbaparse/tgbascan.ll: Process " and \ escapes in
strings.
* src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/tgbaread.test,
src/tgbatest/tripprod.test: Adjust to new syntax for explicit
automata.
(minato_isop::local_vars::vars): New attribute.
(minato_isop::local_vars::local_vars): Add the vars arguments.
(minato_isop::todo, minato_isop::cube, minato_isop::ret): Rename as ...
(minato_isop::todo_, minato_isop::cube_, minato_isop::ret_): ... these.
* src/misc/minato.cc: Adjust to factorize only variables in vars.
