2003-07-03 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first): Simplify, do not call next_non_false_() either side is done. * src/tgba/succiter.hh (tgba_succ_iterator::current_condition): 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. 2003-07-02 Alexandre Duret-Lutz * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New function. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_core_data::translate. * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): 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. Rewrite tgba_succ_iterator_concrete::next for the fourth time (or is it the fifth?). * 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_): New attributes. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::tgba_succ_iterator_concrete): Initialize new members. (tgba_succ_iterator_concrete::first): Likewise. (tgba_succ_iterator_concrete::next): Rewrite. * tgba/tgbabddcoredata.hh (tgba_bdd_core_data::acc_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Handle acc_set. 2003-07-01 Alexandre Duret-Lutz * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Translate varandnext_set. 2003-06-30 Alexandre Duret-Lutz * src/tgbaparse/tgbaparse.yy (lines): Expect at last one line. * doc/Doxyfile.in (HAVE_DOT): Set to YES to output collaboration diagrams. * doc/mainpage.dox: Typo. * src/tgba/state.hh (state::as_bdd): Delete. * src/tgba/tgbaproduct.hh (state_bdd_product): Inherit from state, not state_bdd. (state_bdd_product::state_bdd_product): Adjust. * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): Adjust. * src/tgba/succiter.hh (tgba_bdd_succ_iterator::done): Mark as const. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::done): Likewise. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::done): Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::done): Likewise. * src/tgba/tgbaexplicit.hh (tgba_explicit_succ_iterator::done): Likewise. * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::done): Likewise. * src/tgba/tgbaproduct.hh (tgba_product_succ_iterator::done): Likewise. * src/tgba/tgbatranslateproxy.hh (tgba_translate_proxy_succ_iterator::done): Likewise. * src/tgba/tgbatranslateproxy.cc (tgba_translate_proxy_succ_iterator::done): Likewise. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Call bdd_satoneset on data_.varandnext_set. The previous implementation was wrong for GFa. * src/tgba/tgbabddcoredata.hh: Declare varandnext_set. * src/tgba/tgbabddcoredata.cc: Handle varandnext_set. * doc/Doxygen.in: Enable LaTeX output. * doc/Makefile.am (spotref.pdf): New rule. (EXTRA_DIST): Add spotref.pdf. * src/tgba/tgbabddconcretefactory.cc: (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. 2003-06-28 Alexandre Duret-Lutz Fix errors reported by ICC. * 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. 2003-06-26 Alexandre Duret-Lutz * Makefile.am (EXTRA_DIST): Add HACKING. * configure.ac: Bump version to 0.0c. * configure.ac: Bump version to 0.0b. * INSTALL: New file. * src/tgba/ltl2tgba.hh, src/tgba/ltl2tgba.cc: Move ... * src/tgbaalgos/ltl2tgba.hh, src/tgbaalgos/ltl2tgba.cc: ... here. * src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust. * src/tgba/public.hh: Do not include ltl2tgba.hh. * src/tgbatests/explprod.cc, src/tgbatests/ltl2tgba.cc, src/tgbatests/ltlprod.cc, src/tgbatests/mixprod.cc, src/tgbatests/reach.cc, src/tgbatests/tripprod.cc: Adjust inclusions. * src/tgba/tgbabddcoredata.hh: Fix some Doxygen comments. * src/ltlast/formula.hh: More Doxygen comments. * src/tgba/tgba.hh: Use in Doxygen comments. * doc/mainpage.dox: New file. * doc/Makefile.am (EXTRA_DIST): Add mainpage.dox. * doc/Doxyfile.in (INPUT): Add @srcdir@/mainpage.dox * src/tgba/succiter.hh: Adjust comments about promises to refer to accepting conditions. * src/tgba/tgbabddconcretefactory.hh: Likewise. * src/tgba/tgbabddcoredata.hh: Likewise. * src/tgba/dictunion.cc: Likewise. * src/tgba/tgba.hh: Likewise. * doc/Makefile.am (doc): Typo. * src/ltlvisit/tostring.hh (to_string): Add doxygen comments. * src/ltlast/multop.hh (multop::paircmp): Add doxygen comments. * src/tgba/tgbaexplicit.hh (tgba_explicit::transtion, state_explicit, tgba_explicit_succ_iterator): Add doxygen comments. * src/ltlvisit/postfix.hh: Typo. * src/ltlast/Makefile.am (ltlastdir, ltlast_HEADERS): New variables. (libltlast_la_SOURCES): Move all headers to ltlast_HEADERS. * src/ltlenv/Makefile.am (ltlenvdir, ltlenv_HEADERS): New variables. (libltlenv_la_SOURCES): Move all headers to ltlenv_HEADERS. * src/ltlparse/Makefile.am (ltlparsedir, ltlparse_HEADERS): New variables. (libltlparse_la_SOURCES): Move all public headers to ltlparse_HEADERS. * src/ltlvisit/Makefile.am (ltlvisitdir, ltlvisit_HEADERS): New variables. (libltlvisit_la_SOURCES): Move all headers to ltlparse_HEADERS. * src/misc/Makefile.am (include_HEADERS): Rename as .. (misc_HEADERS): ... this. (miscdir): New variable. * src/tgba/Makefile.am (tgbadir, tgba_HEADERS): New variables. (libtgba_la_SOURCES): Move all headers to tgba_HEADERS. * src/tgbaalgos/Makefile.am (tgbaalgosdir, tgbaalgos_HEADERS): New variables. (libtgbaalgos_la_SOURCES): Move all headers to tgbaalgos_HEADERS. * src/tgbaparse/Makefile.am (tgbaparsedir, tgbaparse_HEADERS): New variables. (libtgbaparse_la_SOURCES): Move all public headers to tgbaparse_HEADERS. * src/tgbaparse/public.hh: Include ltlparse/location.hh, not location.hh. * doc/Makefile.am (stamp): Prefix $(srcdir) explicitely. * m4/buddy.m4 (BUDDY_LDFLAGS): Use $(top_builddir), not $(top_srcdir). * src/tgbaparse/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS). * doc/Makefile.am: Rewrite to run Doxygen whenever Doxyfile.in or configure.ac changes. Distribute the html doc. * doc/Doxyfile.in (EXCLUDE_PATTERNS): Complete with useless Bison classes. (FILE_PATTERNS): Remove *.cc files. Distribute BuDDy. Compile and link with the included version if explicitely requested (--with-included-buddy) or if there is now stuitable version already installed. * buddy/: New directory. Contains a patched version of BuDDy 2.2. * m4/buddy.m4: Make sure the installed BuDDy supports bdd_mergepairs. Honor --with-included-buddy and --without-included-buddy. Define the BUDDY_LDFLAGS and BUDDY_CPPFLAGS output variables, and the WITH_INCLUDED_BUDDY Automake conditional * Makefile.am [WITH_INCLUDED_BUDDY] (MAYBE_SUBDIRS): New variable. (SUBDIRS): Prepend $(MAYBE_SUBDIRS). * src/Makefile.am (libspot_LDFLAGS): New variable. * src/tgba/Makefile.am (AM_CPPFLAGS): Add $(BUDDY_CPPFLAGS). * src/tgbaalgos/Makefile.am (AM_CPPFLAGS): Likewise. * src/tgbatest/Makefile.am (AM_CPPFLAGS): Likewise. 2003-06-25 Alexandre Duret-Lutz * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Rewrite using bdd_satoneset. This time it's for real. (I hope.) * src/tgba/succiterconcrete.hh (current_base_, current_base_left_): Delete. * tgba/tgbabddcoredata.hh (next_set): New variable. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update next_set. * src/tgba/bddprint.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbaproduct.hh: Fix Doxygen comments. * src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ... (succ_set_left_): ... this. (current_base_, current_base_left_): New variables. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first): Reset current_. (tgba_succ_iterator_concrete::next): Rewrite. (tgba_succ_iterator_concrete::current_state): Simplify. (tgba_succ_iterator_concrete::current_accepting_conditions): Remove atomic proposition with universal quantification. * src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state): Complete the initial state. (tgba_bdd_concrete::succ_iter): Do not remove Now variable from the BDD passed to the iterator. * tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust to update notnow_set and var_set. * src/tgbatest/ltl2tgba.cc: Support -v. 2003-06-24 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc (syntax): Fix usage message. * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort accepting conditions. * src/ltlvisit/nenoform.cc (negative_normal_form): New const variant. * src/ltlvisit/nenoform.hh (negative_normal_form): New const variant. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic): New const variant. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic): New const variant. * src/ltlvisit/tunabbrev.cc (unabbreviate_ltl): New const variant. * src/ltlvisit/tunabbrev.hh (unabbreviate_ltl): New const variant. 2003-06-23 Alexandre Duret-Lutz Switch from "promises" to "accepting sets". Fix the definitions of these accepting sets so that they are really useful. Provide an all_accepting_conditions() method for use in the emptyness check, and a neg_accepting_conditions() for products. Predeclare TGBA accepting conditions in the i/o. * src/tgba/bddprint.cc (want_prom): Rename as ... (want_prom): ... this. (print_handler): Adjust to display Acc[]. (print_acc_handler, bdd_print_acc): New functions. * src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc): New functions. * src/tgba/succiter.hh (current_promise): Rename as ... (current_accepting_conditions): ... this. * src/tgba/succiterconcrete.cc (current_state): Rename next to now. (current_promise): Rename as ... (current_accepting_conditions): ... this, and compute the accepting conditions. * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc, src/tgba/tgbabddtranslatefactory.cc, src/tgbaalgos/dotty.cc: Adjust to new names. * src/tgba/tgba.hh (all_accepting_conditions, neg_accepting_conditions): New functions. * src/tgba/tgbabddconcretefactory.cc: Adjust to new names, and record accepting conditions instead of promises. * src/tgba/tgbabddcoredata.hh (accepting_conditions, all_accepting_conditions, negacc_set): New variables. (notnow_set, notprom_set, declare_promise): Rename as ... (notnext_set, notacc_set, declare_accepting_condition): ... these. * src/tgba/tgbaexplicit.hh (tgba_explicit_succ_iterator::current_promise): Rename as ... (tgba_explicit_succ_iterator::current_accepting_conditions): ... this. (tgba_explicit::add_promise): Rename as ... (tgba_explicit::add_accepting_condition): ... this. (tgba_explicit::declare_accepting_condition, tgba_explicit::has_accepting_condition): New variables. (tgba_explicit::get_promise): Rename as ... (tgba_explicit::get_accepting_condition): ... this. (tgba_explicit::all_accepting_conditions, tgba_explicit::neg_accepting_conditions): Implement them. (all_accepting_conditions, neg_accepting_conditions, all_accepting_conditions): New variables. (tgba_explicit_succ_iterator): Embed all_accepting_conditions_. * src/tgba/tgbaexplicit.cc: Likewise. * src/tgba/tgbaproduct.hh (tgba_product_succ_uterator): Embed left_neg_ and right_neg_. (tgba_product::all_accepting_conditions, tgba_product::neg_accepting_conditions): Implement them. * src/tgba/tgbatranslateproxy.hh: (tgba_translate_proxy::all_accepting_conditions, tgba_translate_proxy::neg_accepting_conditions): Implement them. * src/tgba/tgbatranslateproxy.cc: Likewise. * src/tgbaalgos/save.cc (save_rec): Call bdd_print (tgba_save_reachable): Output the `acc =' line. * src/tgbaparse/tgbaparse.yy: Support the for accepting conditions definitions using an "acc =" line at the start. Later, use has_accepting_condition while parsing accepting conditions to ensure they were declared. Disallow !cond in accepting conditions. * src/tgbaparse/tgbascan.ll (ACC_DEF): New token. * src/tgbatest/explicit.cc (main): Declare accepting conditions. * src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A, and -R new options. * src/tgbatest/tgbaread.cc (main): Really exit on parse error. * src/tgbatest/explicit.test, src/tgbatest/explprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect recent changes. 2003-06-22 Alexandre Duret-Lutz * src/tgbatest/tripprod.test, src/tgbatest/explprod.test: Sort out some possible inversions in the output. 2003-06-19 Alexandre Duret-Lutz * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory): destroy the formulae used as keys in prom_. (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::create_promise): Delete. (tgba_bdd_concrete_factory::declare_promise, tgba_bdd_concrete_factory::finish): New functions. (tgba_bdd_concrete_factory::prom_): New map. * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Adjust the Fx and aUb cases to register promises with tgba_bdd_concrete_factory::declare_promise(). (ltl2tgba): Call tgba_bdd_concrete_factory::finish(). * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Revert the change from 2003-06-12, it needs more work (the automaton generated on Xa&(b U !a) was bogus, with that patch). * src/tgbatest/ltl2tgba.cc: Handle the -o and -r options. * src/tgbatest/tripprod.test, src/tgbatest/explprod.test, src/tgbatest/readsave.test: Adjust to reflect yesterday's bddprint.cc change. 2003-06-18 Alexandre Duret-Lutz * src/tgba/bddprint.cc (print_handler): Quote promises when !want_prom. * src/tgbaparse/tgbaparse.yy (prop_list): Accept strings or identifiers. Discard empty strings. * src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add mixprod. (mixprod_SOURCES): New variable. (TESTS): Add mixprod.test. 2003-06-17 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product): New constructor. * src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product): New constructor. * tgbatest/tripprod.cc, tgbatest/tripprod.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (tripprod_SOURCES): New variable. (CLEANFILES): Add input3. (TESTS): Add tripprod.test. 2003-06-16 Alexandre Duret-Lutz * src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ... * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: ... these. (tgba_bdd_product, tgba_bdd_product_succ_iterator): Rename as ... (tgba_product, tgba_product_succ_iterator): ... these, and adjust all uses. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: Rename as ... * src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: ... these. (tgba_bdd_translate_proxy, tgba_bdd_translate_proxy_succ_iterator): Rename as ... (tgba_translate_proxy, tgba_translate_proxy_succ_iterator): ... these, and adjust all uses. Make sure we can multiply two tgba_explicit. * tgba/state.hh (state::translate, state::clone, state::as_bdd): New virtual methods. * tgba/stataebdd.cc (state::translate, state::clone): New methods. * tgba/stataebdd.hh (state::translate, state::clone): New methods. * tgba/tgbabddprod.cc (state_bdd_product::clone, tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): New methods. (tgba_bdd_product_succ_iterator::first): Reset right_ if any of left_ or right_ is already done (i.e., is empty). (tgba_bdd_product_succ_iterator::done): Return true if right_ is NULL. (tgba_bdd_product_succ_iterator::current_state, tgba_bdd_product::get_init_state): Work directory with `state's. * tgba/tgbabddprod.hh (state_bdd_product::clone, tgba_bdd_product_succ_iterator::~tgba_bdd_product_succ_iterator): New methods. * tgba/tgbabddtranslateproxy.cc (tgba_bdd_translate_proxy_succ_iterator:: tgba_bdd_translate_proxy_succ_iterator): Work on any kind of iteraator. (tgba_bdd_translate_proxy_succ_iterator:: ~tgba_bdd_translate_proxy_succ_iterator): New method. (tgba_bdd_translate_proxy_succ_iterator::current_state, tgba_bdd_translate_proxy::get_init_state, tgba_bdd_translate_proxy::succ_iter): Work on `state's and `tgba_succ_iterator's directlry. (tgba_bdd_translate_proxy::format_state): Delegate formating to the proxied automata. * tgba/tgbaexplicit.cc (state_explicit::clone): New method. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise): Call ltl::destroy on existing formulae. * tgbatest/explprod.cc, tgbatest/explprod.test: New files. * tgbatest/Makefile.am (check_PROGRAMS): Add explprod. (explprod_SOURCES): New variable. (TESTS): Add explprod.test. (CLEANFILES): Add input1 and input2. 2003-06-12 Alexandre Duret-Lutz * src/tgba/tgbabddconcrete.cc (set_init_state, succ_iter): Make sure to compute the status of the most Now variables possible. This helps to identify equivalant states. (tgba_bdd_concrete): Call set_init_state. 2003-06-10 Alexandre Duret-Lutz * src/tgba/ltl2tgba.cc (ltl_trad_visitor::visit): Handle F and G. * src/tgbatest/ltl2tgba.test: Use F and G. 2003-06-06 Alexandre Duret-Lutz * src/tgbatest/bddprod.test: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add bddprod. (bddprod_SOURCES, bddprod_CXXFLAGS): New variables. (TESTS): Add bddprod.test. * src/tgbatest/ltlprod.c: Handle BDD_CONCRETE_PRODUCT. * src/tgba/dictunion.cc (tgba_bdd_dict_union): Clone formulae while building new dictionary. * src/tgbatest/ltlprod.test, src/tgbatest/ltlprod.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltlprod. (ltlprod_SOURCES): New variable. (TESTS): Add ltlprod.test. * src/ltlvisit/clone.cc (clone): New const version. * src/ltlvisit/clone.hh (clone): Likewise. * src/ltlvisit/destroy.cc (destroy): New const version. * src/ltlvisit/destroy.hh (destroy): Likewise. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::create_state, tgba_bdd_concrete_factory::create_atomic_prop, tgba_bdd_concrete_factory::promise): Clone new formulae. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::tgba_bdd_dict, tgba_bdd_dict::~tgba_bdd_dict, tgba_bdd_dict::operator=): New methods that clone and destroy formulae. * src/tgbatest/ltl2tgba.test, src/tgbatest/ltl2tgba.cc: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add ltl2tgba. (ltl2tgba_SOURCES): New variable. (TESTS): Add ltl2tgba.test. * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/tgba/bddprint.cc, src/ltltest/tostring.cc: Include . 2003-06-05 Alexandre Duret-Lutz * src/tgba/bddprint.cc (dict): Make this variable static. (want_prom): New global static variable. (print_handle): Honor want_prom. (print_sat_handler, bdd_print_sat, bdd_format_sat): New functions. (bdd_print_set, bdd_print_dot, bdd_print_table): Set want_prom. * src/tgba/bddprint.hh (bdd_print_sat, bdd_format_sat): New functions. * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbatest/readsave.cc, src/tgbatest/readsave.test: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add save.cc and save.hh. * src/tgbatest/Makefile.am (check_PROGRAMS): Add readsave. (readsave_SOURCES): New variable. (TESTS): Add readsave.test. * configure.ac: Output src/tgbaparse/Makefile. * src/Makefile.am (SUBDIRS): Add tgbaparse. (libspot_la_LDADD): Add tgbaparse/libtgbaparse.la. * src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition, tgba_explicit::get_promise, tgba_explicit::add_neg_condition, tgba_explicit::add_neg_promise): New methods. * src/tgba/tgbaexplicit.hh: Declare them. * src/tgbaparse/Makefile.am, src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll, src/tgbatest/tgbaread.cc, src/tgbatest/tgbaread.test: New files. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tgbaread. (TESTS): Add tgbaread.cc. (CLEANFILES): Add input. (tgbaread_SOURCES): New variable. * src/ltlparse/ltlparse.yy: Typo in comment. * configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs. * src/Makefile.am (SUBDIRS): Add tgbatest. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc and tgbaexplicit.hh. * src/tgbatest/Makefile.am, src/tgbatest/defs.in, src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files. 2003-06-04 Alexandre Duret-Lutz * src/ltlparse/ltlparse.yy (result): Suppress unused definition. * src/Makefile.am (SUBDIRS): Build `ltltest' after `.'. * src/ltlparse/ltlscan.ll: Use ltlyy as %prefix. * src/ltlparse/parsedecl.hh (YY_DECL): Rename yylex to ltlyylex. * src/ltlparse/ltlparse.yy: Define yylex as ltlyylex. 2003-06-03 Alexandre Duret-Lutz * src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc, src/tgba/succiterconcrete.cc, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddprod.cc, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbabddtranslateproxy.cc: Include . 2003-06-02 Alexandre Duret-Lutz * src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/tgbabdddict.cc (tgba_bdd_dict::contains): New function. * src/tgba/tgbabdddict.hh (tgba_bdd_dict::contains): Likewise. 2003-05-28 Alexandre Duret-Lutz * src/tgba/statebdd.hh (state_bdd::as_bdd): Add non-const variant. * src/tgba/tgbabddtranslateproxy.cc, src/tgba/tgbabddtranslateproxy.hh: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. 2003-05-27 Alexandre Duret-Lutz * src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbabddtranslatefactory.hh, src/tgbaalgos/dotty.cc: Add Doxygen comments. * src/tgba/bddfactory.hh, src/tgba/statebdd.hh, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.hh: Add Doxygen comments. * src/tgba/bddprint.hh (bdd_format_set): New function. * src/tgba/bddprint.cc (bdd_format_set): Likewise. * src/tgba/state.hh: Add Doxygen comments. (state::compare): Take a state*, not a state&. (state_ptr_less_than): New functor. * src/tgba/statebdd.hh (state_bdd::compare): Take a state*, not a state&. * src/tgba/statebdd.cc (state_bdd::compare): Likewise. * src/tgba/succiter.hh: Add Doxygen comments. * src/tgba/tgba.hh: Mention promises. (tgba::formate_state): New pure virtual method. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::formate_state): New method. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::formate_state): Likewise. * src/tgbaalgos/dotty.cc: Adjust to use state_ptr_less_than and tgba::formate_state. * src/tgba/succiter.hh (tgba_succ_iterator::current_state): Return a state*, not a state_bdd. * src/tgba/succiterconcrete.hh (tgba_succ_iterator_concrete::current_state): Return a state_bdd*, not a state_bdd. * src/tgba/tgba.hh: Add Doxygen comments. (tgba::succ_iter, tgba::get_init_state): Use state*, not state_bdd. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete::get_init_state): Return a state_bdd*, not a state_bdd. (tgba_bdd_concrete::get_init_bdd): New method. (tgba_bdd_concrete::succ_uter): Take a state* as argument. * src/tgba/tgbabddconcrete.cc: Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_concrete::get_init_bdd. * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty): Adjust to use state* instead of state_bdd. * src/tgba/succlist.hh: Delete. (Leftover from a previous draft.) 2003-05-26 Alexandre Duret-Lutz * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES): Add them. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::compute_pairs): Be quiet. * src/Makefile.am (SUBDIRS): Add tgbaalgos. (libspot_la_LIBADD): Add tgba/libtgbaalgos. * src/tgbaalgos/Makefile.am: New file. * configure.ac: Output src/tgbaalgos/Makefile. * src/tgba/bddprint.hh, src/tgba/bddprint.cc: New files. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add them. * src/tgba/public.hh: Include bddprint.hh. * src/tgba/tgba.hh: Rename as ... * src/tgba/public.hh: .. this. * src/tgba/tgba.hh: New file. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add public.hh. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Inherit from tgba. (tgba_bdd_concrete::init_iter): Delete. (tgba_bdd_concrete::succ_iter): Take a state_bdd as argument, not a bdd. * src/tgba/tgbabddconcrete.cc: Likewise. Initial code for TGBA (Transition Generalized Büchi Automata). Contains tgba_bdd, a BDD-encoded TGBA, and ltl_to_tgba, a LTL-to-TGBA translator using Couvreur's algorithm. * src/Makefile.am (SUBDIRS): Add tgba. (libspot_la_LIBADD): Add tgba/libtgba.la. * configure.ac: Output src/tgba/Makefile. * src/tgba/Makefile.am, src/tgba/bddfactory.cc, src/tgba/bddfactory.hh, src/tgba/dictunion.cc, src/tgba/dictunion.hh, src/tgba/ltl2tgba.cc, src/tgba/ltl2tgba.hh, src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiter.hh, src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/succlist.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabdddict.cc, src/tgba/tgbabdddict.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbabddtranslatefactory.hh: New files. 2003-05-23 Alexandre Duret-Lutz * m4/gccwarn.m4: Do not use -Winline, this is inappropriate with STL. * src/ltlast/atomic_prop.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc: Include . 2003-05-16 Alexandre Duret-Lutz * src/ltlvisit/dotty.cc: Rewrite to display formulae as graphs rather than trees, to show how nodes are shared. * src/ltlvisit/dump.hh (dump): Return the passed ostream. * src/ltlvisit/dump.cc (dump): Likewise. * src/ltlvisit/dotty.hh (dotty): Likewise. * src/ltlvisit/dotty.cc (dotty): Likewise. * src/ltlvisit/tostring.hh (to_string): Likewise. * src/ltlvisit/tostring.cc (to_string): Likewise. * src/ltlvisit/dump.hh (dump): Take a formula* as argument, not a formula&. This is more homogeneous. * src/ltlvisit/dump.cc (dump): Likewise. * src/ltlvisit/dotty.hh (dotty): Likewise. * src/ltlvisit/dotty.cc (dotty): Likewise. * src/ltlvisit/tostring.hh (to_string): Likewise. * src/ltlvisit/tostring.cc (to_string): Likewise. * src/ltltest/readltl.cc, src/ltltest/equals.cc, src/ltltest/tostring.cc: Adjust usage. Check trivial multop equality at build time. This makes the equal visitor useless, since two equals formulae will now share the same address. * src/ltlast/multop.hh (add_sorted): New function. (paircmp): New comparison functor. (map): Use paircmp, we want to compare the vectors' contents, not their addresses. * src/ltlast/multop.cc (add_sorted): New function. (add): Use it. * src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare pointers instead of calling equal. * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove equals.cc and equals.hh. * wrap/spot.i: Do not include equals.hh. 2003-05-15 Alexandre Duret-Lutz Implement spot::ltl::destroy() and exercise it. * src/ltlast/atomic_prop.hh: Declare instance_count(). * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh: Likewise. Also, really inherit for ref_formula this time. * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress the instance from the instance map. Implement instance_count(). * src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual destructors. * src/ltlparse/ltlparse.yy: Recover from binary operators with missing right hand operand (the point is just to destroy the the left hand operand). * src/ltltest/equals.cc, src/ltltest/readltl.cc, src/ltltest/tostring.cc: Destroy used formulae. Make sure instance_count()s are null are the end. * src/ltltest/parseerr.test: Adjust expected result, now that the parser lnows about missing right hand operands. * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc, src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them. * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae occurring twice in the rewritten expression. Massage the AST so that identical sub-formula share the same reference-counted formula*. One can't call constructors for AST items anymore, everything need to be acquired through instance() class methods. * src/ltlast/formula.cc, src/ltlast/refformula.cc, src/ltlast/refformula.hh: New files. * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them. * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor and destructor protected. Define a static function `instance()' to get an instance with specific argument. Use a map called `instances' to store all known instances. Inherit from ref_formula. * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect the constructor and destructor. Provide the false_instance() and true_instance() functions instead. * src/formula.hh (ref, unref, ref_, unref_): New methods. * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect the constructor, destructor, as well as the add() method. Provides the instance(), and add() class methods instead. Store children_ as a pointer. * src/ltlenv/defaultenv.cc (require): Adjust to call atomic_prop::instance. * src/ltlparse/ltlparse.yy: Adjust to call instance() functions instead of constructors. * src/ltltest/Makefile.am (LDADD): Tweak library ordering. * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor, not const_visitor, and adjust all prototypes appropriately. * src/ltlvisit/clone.cc (clone_visitor): Likewise. Call ref() or instance() methods instead of copy constructors. * src/ltlvisit/equals.cc: Simplify atomic_prop and constant cases. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc, src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc, src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance() methods instead of constructor. Make these children of visitor, not const_visitor. * src/ltltest/readltl.c (main): Do not delete the formula. * src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to remove a warning with newer versions of Flex. * src/ltlparse/ltlparse.yy (error_list, parse_environment, result): CVS Bison now supports %parse-param for the C++ skeleton; pass these variables as arguments to the Parser::Parser constructor instead of using globals. (parse): Adjust Parser::Parser call. 2003-05-12 Alexandre Duret-Lutz * src/ltlvisit/tostring.cc: Reindent and strip out superfluous spot::ltl:: prefixes. (to_string(formula)): New function. * src/ltlvisit/tostring.hh (to_string(formula)): Likewise. * src/ltltest/tostring.cc: Use this new to_string function to simplify. 2003-05-05 Alexandre Duret-Lutz * m4/buddy.m4: New file. * Makefile.am (EXTRA_DIST): Add m4/buddy.m4. * configure.ac: Call AX_CHECK_BUDDY. 2003-04-30 Alexandre Duret-Lutz * src/ltlvisit/Makefile.am (lib_LTLIBRARIES): Rename as ... (noinst_LTLIBRARIES): ... this. * src/ltlenv/Makefile.am, src/ltlast/Makefile.am, src/ltlparse/Makefile.am: Likewise. * src/Makefile.am (lib_LTLIBRARIES, libspot_la_SOURCES, libspot_la_LIBADD): New variable. Build a libspot.la library from all the sub-libraries. * m4/pypath.m4: New file. * Makefile.am (SUBDIRS): Add wrap. * wrap/Makefile.am: New file. * wrap/spot.i: New file. Preliminary bindings for Python. * configure.ac: Call adl_CHECK_PYTHON and output wrap/Makefile. 2003-04-29 Alexandre Duret-Lutz * configure.ac: Call AC_PROG_LIBTOOL. * src/ltlast/Makefile.am, src/ltlenv/Makefile.am, src/ltlparse/Makefile.am, src/ltltest/Makefile.am, src/ltlvisit/Makefile.am: Adust to build libtool libraries. * src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here... * src/ltlenv/defaultenv.cc: ... but here. * src/ltltest/tostring.test: Simplify with set -e. Move the description of the test ... * src/ltltest/tostring.cc: ... here, where it is actually coded. * src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test, src/ltltest/nenoform.test, src/ltltest/tunenoform.test: Simplify with set -e. * configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make sure we always use paths relative to src/ in src/'s subdirectories. 2003-04-28 Alexandre Duret-Lutz * src/ltlparse/Makefile.am (CXXFLAGS): Turn on GCC warnings now that CVS Bison is fixed. * src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning. 2003-04-24 Rachid REBIHA * src/ltltest/tostring.test: New file. * src/ltltest/tostring.cc: New files. * src/ltlvisit/tostring.hh: From ast to string New files. * src/ltlvisit/tostring.cc: From ast to string New files. 2003-04-18 Alexandre Duret-Lutz * src/ltlparse/Makefile.am (EXTRA_DIST): Distribute ltlparse.yy. * src/ltlast/Makefile.am (libltlast_a_SOURCES): Add visitor.hh. * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/public.hh, src/ltlvisit/clone.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/equals.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/tunabbrev.hh: Add Doxygen comments. * src/visitor.hh: Do not use const_sel. This clarifies the code and helps Doxygen. * configure.ac: Output doc/Doxyfile and doc/Makefile. * doc/Makefile.am, doc/Doxyfile.in: New files. * Makefile.am (SUBDIRS): Add doc. * src/ltlparse/ltlscan.ll: Recognize && and ||. * src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/equals.test: Use these operators.. 2003-04-17 Alexandre Duret-Lutz * src/ltltest/readltl.cc, src/ltltest/equals.cc: Cosmetics. * src/ltlenv/environment.hh (require): Return a formula, not an atomic_prop. * src/ltlast/atomic_prop.hh (atomic_prop): New argument env. (environment_): New member. (env): New method. * src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise. * src/ltlenv/defaultenv.cc (require): Pass *this as the environment argument to atomic_prop. * src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy the environment. * src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise. * configure.ac: Output src/ltlenv/Makefile. * src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files. * src/ltlparse/public.hh (parse): Take an environment as third argument. * src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the atomic proposition via the environment. * src/ltltest/readltl.cc (main): Adjust the call to parse(). * src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a. * src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit from clone_visitor and remove all useless methods (now inherited). * src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form. * src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and tunenoform. (nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES, tunenoform_CPPFLAGS): New variables. (TESTS): Add nenoform.test and tunenoform.test. * src/ltlvisit/lunabbrev.hh: Fix include guard. 2003-04-16 Alexandre Duret-Lutz * src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/tunabbrev.test: New file. * src/ltltest/lunabbrev.test: Fix comment. * src/ltltest/Makefile.am (TESTS): Add tunabbrev.test. (check_PROGRAMS): Add tunabbrev. (tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse): New virtual function. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse): Likewise. (unabbreviate_logic_visitor::visit): Use it instead of calling unabbreviate_logic directly. * src/ltlvisit/lunabbrev.hh: Add missing include guard. * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlast/multop.cc (multop::multop(type)): New constructor. * src/ltlast/multop.hh (multop::multop(type)): New constructor. * src/ltltest/lunabbrev.test: New file. * src/ltltest/Makefile.am (TESTS): Add lunabbrev.test. (check_PROGRAMS): Add lunabbrev. (lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic. * src/ltltest/equals.test (check0, check1): Remove. Use check 0, and check 1 instead. * src/ltlast/formulae.hh: Rename as ... * src/ltlast/formula.hh: ... this. * src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust. * src/ltlast/formula.hh (formulae): Rename as ... (formula): ... this. Adjust all uses. * src/ltlparse/public.hh (format_parse_errors): New function. * src/ltlparse/fmterror.cc: New file. * src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc. * src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using format_parse_errors. * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh and equals.cc. * src/ltltest/equals.cc, src/ltltest/equals.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add equals. (equals_SOURCES): New variable. (TESTS): Add equals.test. * src/ltlast/multop.cc (multop::multop): Use multop::add. (multop::add): If the formulae we add is itself a multop for the same operator, merge its children with ours. * src/ltltest/parseerr.test: Add two tests for multop merging. 2003-04-15 Alexandre Duret-Lutz * src/ltlast/formulae.hh (formulae::equals): Remove. * src/ltlast/unop.hh (unop::equals): Remove. * src/ltlast/unop.cc (unop::equals): Remove. * src/ltlast/binop.hh (binop::equals): Remove. * src/ltlast/binop.cc (binop::equals): Remove. * src/ltlast/multop.hh (multop::equals): Remove. * src/ltlast/multop.cc (multop::equals): Remove. * src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove. * src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove. * src/ltlast/constant.hh (constant::equals): Remove. * src/ltlast/constant.cc (constant::equals): Remove. * HACKING, Makefile.am, configure.ac, m4/gccwarn.m4, src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh, src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh, src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formulae.hh, src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/ltlvisit/Makefile.am, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh, src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc, src/ltltest/parse.test, src/ltltest/parseerr.test, src/misc/Makefile.am, src/misc/const_sel.hh: New files.