not create Now/Next variable when G is the root of the formula.
(ltl_trad_visitor::ltl_trad_visitor): Take a root argument.
(ltl_trad_visitor::recurse): Create a new visitor, do not copy
the current one.
(ltl_to_tgba): Build ltl_trad_visitor with root = true.
* src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::X)):
Remove FIXME about handling X(a U b) and X(a R b) better, it's
done naturally.
Fix so that !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f]
is factored as !p.!Acc[g].Acc[f] + p.(!Acc[g].Acc[f] + Acc[g].!Acc[f]),
not !Acc[g].Acc[f] + p.Acc[g].!Acc[f].
Declare class SpotWrapper as a friend.
* src/SpotWrapper.h, src/SpotWrapper.cc: New files.
* src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc
and SpotWrapper.h.
* src/translate.cc (main): Add the --spot option, and build
a SpotWrapper of required.
* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
to designate initial states.
(lbtt_reachable): Adjust calls to fill_todo. Handle the
fake initial state accepting conditions specially.
* src/tgbaalgos/lbtt.hh: Update comments.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh.
(libtgbaalgos_la_SOURCES): Add lbtt.cc.
* src/tgba/bddprint.cc (print_sat_handler): Put a space after "!".
* src/tgbatest/readsave.test: Adjust spaces after "!".
(tgba_succ_iterator_concrete::current_acc_): New attribute.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Set current_acc_.
(tgba_succ_iterator_concrete::current_accepting_conditions):
Simply return it.
State that this is a boolean function.
* src/tgba/succiterconcrete.hh
(tgba_succ_iterator_concrete::trans_dest_,
tgba_succ_iterator_concrete::trans_set_,
tgba_succ_iterator_concrete::trans_set_left_,
tgba_succ_iterator_concrete::neg_trans_set_): Remove.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::tgba_succ_iterator_concrete,
tgba_succ_iterator_concrete::first): Adjust to removed members.
(tgba_succ_iterator_concrete::next): Simplify, transitions
are no labelled by boolean functions, not only conjunctions.
Suggested by Denis Poitrenaud.
New attribute.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc:
Handle nownext_set.
* src/tgba/succiterconcrete.cc
(tgba_succ_iterator_concrete::next): Use nownext_set to simplify.
(tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New.
(tgba_bdd_concrete_factory::create_state): Update now_to_next_.
(tgba_bdd_concrete_factory::finish): Constraint Next variables
in the relation.
* src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::now_to_next_): New variable.
(tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New.
(tgba_bdd_concrete_factory::create_state): Update now_to_next_.
(tgba_bdd_concrete_factory::finish): Constraint Next variables
in the relation.
* src/tgba/tgbabddconcretefactory.hh
(tgba_bdd_concrete_factory::now_to_next_): New variable.
* src/tgba/state.hh (state_ptr_less_than::operator()): Make it const.
* src/tgba/tgbaproduct.cc: Include string.hh.
* src/ltlast/multop.hh (multop::add, multop::add_sorted): Do
not use qualified names in declarations.
* m4/gccwarn.m4 (CF_GXX_WARNINGS): Fix GXX test.
* src/ltlenv/defaultenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/environment.hh: Add virtual destructors.
