2003-08-04 Alexandre Duret-Lutz * wrap/python/Makefile.am (lib_LTLIBRARIES) (libspotswigpy_la_SOURCES, libspotswigpy_la_CFLAGS) (libspotswigpy_la_LDFLAGS): New variables. (_spot_la_LIBADD, _buddy_la_LDFLAGS): Link with libspotswigpy.la ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Run swig with -c. * wrap/python/tests/libpy.c: New file. * wrap/python/tests/run.in: Run python if no arguments are given. * wrap/python/tests/interdep.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add interdep.py. * wrap/python/spot.i: Declare spot::ltl_to_tgba as a constructor. * wrap/python/tests/ltl2tgba.py: Do not force `thisown=1' on tgba objects. * wrap/python/spot.i: Include headers from tgba/ and tgbaalgos/. * wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: New files. * wrap/python/tests/Makefile.am (TESTS): Add ltl2tgba.test. (EXTRA_DIST): Add ltl2tgba.py. * wrap/python/tests/run.in: Distinguish *.py and *.test. * wrap/python/tests/ltlparse.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. 2003-08-01 Alexandre Duret-Lutz * wrap/python/buddy.i: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add it. (python_PYTHON, MAINTAINERCLEANFILES): Add buddy.py. (pyexec_LTLIBRARIES): Add _buddy.la. (_buddy_la_SOURCES, _buddy_la_LDFLAGS, $(srcdir)/buddy_wrap.cxx) ($(srcdir)/buddy.py): New. * wrap/python/tests/bddnqueen.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add it. * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the two unabbreviate_logic definitions (const and non-const) into a function that takes a const formula* and return a non-const formula*. Since formula* is convertible to const formula*, and the const version of the function just called the non-onst one, it makes no sense to keep both. Also, it confused Swig. * src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh: Likewise for negative_normal_form. * src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: Likewise for unabbreviate_ltl. * src/ltlvisit/clone.cc, src/ltlvisit/clone.hh: Likewise for clone. * src/ltlvisit/destroy.cc, src/ltlvisit/destroy.hh: Likewise for destroy. * configure.ac: Bump version to 0.0g. * configure.ac, NEWS: Bump version to 0.0f. * iface/gspn/simple.test, iface/gspn/dcswave.test, iface/gspn/dcswaveltl.test: Make sure the example directory is writable. * m4/lbtt.m4, m4/buddy.m4: Always configure buddy/ and lbtt/, regardless of the --with-included-buddy and --with-included-lbtt settings. * wrap/python/Makefile.am (python_PYTHON, _spot_la_SOURCES): Explicitely refer to spot_wrap.cxx and spot.py as $(srcdir)/spot_wrap.cxx and $(srcdir)/spot.py. (spot_wrap.cxx, spot.py): * wrap/python/Makefile.am (spot_wrap.cxx, spot.py): Lookup spot.i in $(srcdir). 2003-07-31 Alexandre Duret-Lutz * configure.ac: Output wrap/python/tests/Makefile and wrap/python/tests/run. * wrap/python/Makefile.am (SUBDIRS): New variable. * wrap/python/spot.i: Include all formulae headers from ltlast/, as well as ltlvisit/destroy.hh. (spot::ltl::formula::__cmp__, spot::ltl::formula::__str__): New functions. * wrap/python/tests/Makefile.am, wrap/python/tests/ltlsimple.py, wrap/python/tests/run.in: New files. * wrap/python/ltihooks.py: New file. * wrap/python/Makefile.am (EXTRA_DIST): Add ltihooks.py. * wrap/Makefile.am, wrap/spot.i: Move ... * wrap/python/Makefile.am, wrap/python/spot.i: ... here. * wrap/Makefile.am: New file. * configure.ac: Output wrap/python/Makefile. * src/misc/const_sel.hh: Delete. * src/misc/Makefile.am (misc_HEADERS): Remove const_sel.hh. * src/tgbaalgos/magic.cc, src/tgbaalgos/reachiter.cc: Include cassert. * iface/Makefile.am (SUBDIRS): Recurse in gspn only if condition WITH_GSPN. 2003-07-30 Alexandre Duret-Lutz * iface/gspn/gspn.cc (tgba_gspn::format_state): Call gspn's print_state. * iface/gspn/dcswaveltl.test: Check for a false formula too. * iface/gspn/dcswaveltl.test, iface/gspn/ltlgspn.cc: New files. * iface/gspn/Makefile.am (TESTS): Add dcswaveltl.test. (ltlgspn_rg_LDADD, ltlgspn_srg_LDADD, ltlgspn_rg_SOURCES) (ltlgspn_srg_SOURCES): New variables. (check_PROGRAMS): Add ltlgspn-rg and ltlgspn-srg. * iface/gspn/Makefile.am (gspn_HEADERS, gspndir): Install gspn.hh. * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::project_state): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::project_state): New method. * src/tgba/tgbabta.hh, src/tgba/tgbabta.cc (tgba_bta_proxy::project_state): New method. * src/tgbaalgos/magic.cc (magic_search::print_result): Take a restrict argument. 2003-07-29 Alexandre Duret-Lutz * src/ltlparse/ltlscan.ll: Allow /\, \/, and xor, used in LBTT. * src/ltltest/parse.test: Test them. * src/tgbaalgos/lbtt.cc: Typos. * lbtt/: Upgrade to lbtt 1.0.2. * src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt. (tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables. * src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally. * src/tgbatest/spotlbtt.test: Include tbalbtt in the tests. 2003-07-28 Alexandre Duret-Lutz * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::state_is_accepting): New method. * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc: New files. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, tgbaalgos_HEADERS): Add them. * src/tgbatest/ltlmagic.cc, src/tgbatest/ltlmagic.test: New files. * src/tgbatest/Makefile.am (TESTS, ltlmagic_SOURCES, check_PROGRAMS): Add them. 2003-07-25 Alexandre Duret-Lutz * src/tgba/tgba.hh (tgba::~tgba): Make it public. * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files. * src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh. (libtgba_la_SOURCES): Add tgbatba.cc. * src/tgbatest/ltl2tgba.cc: Add option -D. * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... * src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. * iface/gspn/dcswave.test: Comment state space sizes. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. (libtgbaalgos_la_SOURCES): Add reachiters.cc. * src/tgbaalgos/dotty.cc, src/tgbaalgos/save.cc: Rewrite using spot::tgba_reachable_iterator_breadth_first. * src/tgbatest/explicit.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust expected output. 2003-07-24 Alexandre Duret-Lutz * configure.ac: Output iface/gspn/defs. * iface/gspn/Makefile.am (EXTRA_DIST): Add $(TESTS). (TESTS, check_SCRIPTS, distclean-local): New. * iface/gspn/dcswave.test, iface/gspn/simple.test, iface/gspn/defs.in: New files. * iface/gspn/dottygspn.cc (main): Take the list of properties of interest in argument. 2003-07-23 Alexandre Duret-Lutz * iface/gspn/examples/DCSwave/DCSWave.def, iface/gspn/examples/DCSwave/DCSWave.net iface/gspn/examples/DCSwave/DCSWave.tobs, iface/gspn/examples/simple/simple.def, iface/gspn/examples/simple/simple.net, iface/gspn/examples/simple/simple.tobs: New files, from Yann Thierry-Mieg. * iface/gspn/Makefile.am (EXTRA_DIST): New variables. * iface/gspn/gspn.cc (tgba_gspn_private_::tgba_gspn_private_): Rethrow caught expections. 2003-07-22 Alexandre Duret-Lutz * m4/gspnlib.m4: Check for libgspnRG.a and libgspnSRG.a. Define LIBGSPNRG_LDFLAGS and LIBGSPNSRG_LDFLAGS, not LIBGSPN_LDFLAGS. * iface/gspn/Makefile.am: Adjust, build dottygspn-rg and dottygspn-srg instead of dottygspn. * iface/gspn/gspn.cc (EVENT_TRUE): Undefine. (tgba_gspn_private_::~tgba_gspn_private_): Free all_indexes. * iface/gspn/dottygspn.cc (main): Destroy the automaton before its dictionnary. 2003-07-17 Alexandre Duret-Lutz Now succ_iter() can fetch extra information from the root of a product to reduce its number of successors. * src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgba.cc. * src/tgba/tgba.hh (tgba::succ_iter): Add the global_state and global_automaton arguments. (tgba::support_conditions, tgba::support_variables, tgba::compute_support_conditions, tgba::compute_support_variables): New functions. (tgba::last_support_conditions_input_, tgba::last_support_conditions_output_, tgba::last_support_variables_input_, tgba::last_support_variables_output_): New attributes. * src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::succ_iter): Handle the two new arguments. (tgba_bdd_concrete::compute_support_conditions, tgba_bdd_concrete::compute_support_variables): Implement them. * src/tgba/tgbabddconcrete.hh: Adjust. * src/tgba/tgbaexplicit.cc (tgba_explicit::succ_iter): Ignore the two new arguments. (tgba_explicit::compute_support_conditions, tgba_explicit::compute_support_variables): Implement them. * src/tgba/tgbaexplicit.hh: Adjust. * src/tgba/tgbaproduct.cc (tgba_product::succ_iter): Handle the two new arguments. (tgba_product::compute_support_conditions, tgba_product::compute_support_variables): Implement them. * src/tgba/tgbaproduct.hh: Adjust. * iface/gspn/gspn.cc (tgba_gspn_private_::last_state_cond_input, tgba_gspn_private_::last_state_cond_output, (tgba_gspn_private_::tgba_gspn_private_): Set last_state_cond_input. (tgba_gspn_private_::~tgba_gspn_private_): Delete last_state_cond_input. (tgba_gspn_private_::state_conds): New function, eved out from tgba_gspn::succ_iter. (tgba_gspn::succ_iter): Use it. Use the two new arguments. (tgba_gspn::compute_support_conditions, tgba_gspn::compute_support_variables): New functions. * iface/gspn/gspn.hh: Adjust. * iface/gspn/gspn.cc (EVENT_TRUE): Override temporarily. (tgba_gspn::succ_iter): Fix usage of cube. 2003-07-16 Alexandre Duret-Lutz * m4/gspnlib.m4: New file. * configure.ac: Call AX_CHECK_GSPNLIB. * Makefile.am (EXTRA_DIST): Add m4/gspnlib.m4. * iface/gspn/Makefile.am (AM_CPPFLAGS): Add $(LIBGSPN_CPPFLAGS). (libspotgspn_la_LIBADD, check_PROGRAMS, dottygspn_SOURCES, dottygspn_LDADD): New variables. * iface/gspn/gspn.hh (gspn_interface): New class. (gspn_exeption): Take a string argument and adjust all callers. (operator<<): Define for gspn_exeption. * iface/gspn/gspn.cc (gspn_interface::gspn_interface, gspn_interface::~gspn_interface): New. * iface/gspn/gspnlib.h: Delete, it belongs to GSPN. * iface/gspn/dottygspn.cc: New file. 2003-07-15 Alexandre Duret-Lutz * m4/lbtt.m4 (AX_CHECK_LBTT): Set LBTT and LBTT_TRANSLATE when using an already installed lbtt. Homogenize passing of automata as pointers, not references. Disallow copy for security. * src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy. * src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise. * src/tgba/tgbaexplicit.cc (tgba_explicit::operator=, tgba_explicit::tgba_explicit(tgba_explicit)): Remove. * src/tgba/tgbabddconcreteproduct.cc (tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory, product): Take operand automata as pointers. * src/tgba/tgbabddconcreteproduct.hh (product): Likewise. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: (tgba_product): Disallow copy. (tgba_product::tgba_product): Take operand automata as pointers. * src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable): Take tgba arguments as pointer. * src/tgbaalgos/dotty.hh (dotty_reachable): Likewise. * src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise. * src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise. * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba): Likewise. * src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise. * src/tgbaalgos/save.hh (save): Likewise. * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Likewise. 2003-07-14 Alexandre Duret-Lutz Before this change, all automata would construct their own dictionaries (map of BDD variables to LTL formulae). This was cumbersome, because to multiply two automata we had to build a common dictionary (the union of the two LTL formula spaces), and install wrappers to translate each automaton's BDD answers into the common dictionary. This translation, that had to be repeated when several products were nested, was time consuming and was a hindrance for some optimizations. In the new scheme, all automata involved in a product must share the same dictionary. An empty dictionary should be constructed by the user and passed to the automaton' constructors as necessary. This huge change removes more code than it adds. * src/Makefile.am (libspot_la_LIBADD): Add misc/libmisc.la. * src/misc/bddalloc.hh, src/misc/bddalloc.cc: New files. These partly replace src/tgba/bddfactory.hh and src/tgba/bddfactory.cc. * src/misc/Makefile.am: Adjust to build bddalloc.hh and bddalloc.cc. * src/tgba/bddfactory.hh, src/tgba/bddfactory.cc, src/tgba/dictunion.hh, src/tgba/dictunion.cc, src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc, src/tgba/tgbabddtranslatefactory.hh, src/tgba/tgbabddtranslatefactory.cc, src/tgba/tgbatranslateproxy.hh, src/tgba/tgbatranslateproxy.cc: Delete. * src/tgba/bdddict.hh, src/tgba/bdddict.cc: New files. These replaces tgbabdddict.hh and tgbabdddict.cc, and also part of bddfactory.hh and bddfactory.cc. * src/tgba/bddprint.cc, src/tgba/bddprint.hh: Adjust to use bdd_dict* instead of tgba_bdd_dict&. * src/tgba/succiterconcrete.cc (succ_iter_concrete::next()): Get next_to_now from the dictionary. * src/tgba/tgba.hh (tgba::get_dict): Return a bdd_dict*, not a const tgba_bdd_dict*. * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh: Adjust to use the new dictionary, stored in data_. * src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh: Likewise. Plus now_to_next_ is now also stored in the dictionary. * src/tgba/tgbabddconcreteproduct.cc: Likewise. Now that both operand share the same product, there is not point in using tgba_bdd_translate_factory. * src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Store a bdd_dict (taken as constructor argument). (tgba_bdd_core_data::~tgba_bdd_core_data): Remove. (tgba_bdd_core_data::translate): Remove. (tgba_bdd_core_data::next_to_now): Remove (now in dict). (tgba_bdd_core_data::dict): New pointer. * src/tgba/tgbabddfactory.hh: (tgba_bdd_factory::get_dict): Remove. * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Adjust to use the new dictionary. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Likewise. Do not use tgba_bdd_dict_union and tgba_bdd_translate_proxy anymore. * src/tgbaalgos/lbtt.cc, src/tgbaalgos/save.cc: Adjust to use bdd_dict* instead of tgba_bdd_dict&. * src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.cc: Likewise. (ltl_to_tgba): Take a dict argument. * src/tgbaparse/public.hh (tgba_parse): Take a dict argument. * src/tgbaparse/tgbaparse.yy (tgba_parse): Take a dict argument. * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc, src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Instantiate a dictionary, and pass it to the automata' constructors. * src/tgbatest/ltl2tgba.cc: Likewise, and remove the -o (defrag) option. * iface/gspn/gspn.hh (tgba_gspn::tgba_gspn): Take a bdd_dict argument. (tgba_gspn::get_dict): Adjust return type. * iface/gspn/gspn.cc: Do not use bdd_factory, adjust to use the new dictionary instead. 2003-07-13 Alexandre Duret-Lutz * configure.ac: Bump version to 0.0e. * configure.ac: Bump version to 0.0d. * NEWS, README: New files. 2003-07-12 Alexandre Duret-Lutz * m4/lbtt.m4: Run lbtt-translate, not lbtt. * iface/gspn/gspn.cc: Include cassert. 2003-07-10 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(multop)): Forward root_ to children of And. (ltl_trad_visitor::recurse): Take a root argument. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory::add_relation): Rename as ... (tgba_bdd_concrete_factory::constrain_relation): ... this. * src/tgba/tgbabddconcretefactory.cc, src/tgbaalgos/ltl2tgba.cc: Adjust. * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit(unop::G)): Do 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. * src/tgbatest/spotlbtt.test: Make 100 rounds. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): 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]. 2003-07-09 Alexandre Duret-Lutz * lbtt/: New directory. Contains a patched version of lbtt 1.0.1. * Makefile.am (MAYBE_LBTT): New variables. (SUBDIRS): Add $(MAYBE_LBTT). (EXTRA_DIST): Add m4/lbtt.m4. * configure.ac: Call AX_CHECK_LBTT. * m4/lbtt.m4: New file. * src/tgbatest/Makefile.am (check_PROGRAMS): Add spotlbtt. (spotlbtt_SOURCES): New variables. (TESTS): Add spotlbtt.test. (CLEANFILE): Add config. * src/tgbatest/defs.in (top_builddir, LBTT, LBTT_TRANSLATE): New substitutions. * src/tgbatest/spotlbtt.cc, src/tgbatest/spotlbtt.test: New files. * src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::next): Fix computation of states sharing the same accepting set. Make sure we only output one initial state in LBTT's output. * 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 (lbtt_reachable): Do not end transitions guards with -1 in output. 2003-07-08 Alexandre Duret-Lutz * src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata. * 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 "!". * src/ltlvisit/dump.cc: Strip useless spot::ltl:: prefixes. 2003-07-07 Alexandre Duret-Lutz First sketch of the GSPN wrapper objects. * iface/gspn/gspn.cc, iface/gspn/gspn.hh: New files. * iface/gspn/Makefile.am (libspotgspn_la_SOURCES): Add them. * src/tgba/succiter.hh (current_state, current_conditions current_accepting_conditions): Mark as const. * src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh, src/tgba/tgbatranslateproxy.cc, src/tgba/tgbatranslateproxy.hh: Likewise. * iface/gspn/gspnlib.h: Fit 80 columns. [__cplusplus]: Wrap everything under extern "C". * src/tgba/succiterconcrete.hh (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. * configure.ac: Output iface/Makefile and iface/gspn/Makefile. * iface/Makefile.am, iface/gspn/Makefile.am: New files. * Makefile.am (SUBDIRS): Add iface. * iface/gspn/gspnlib.h: New file, from Yann and Souheib. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::tgba_bdd_core_data, tgba_bdd_core_data::translate): Handle all_accepting_conditions. * src/tgba/tgbabddconcretefactory.cc (tgba_bdd_concrete_factory::finish): Fill all_accepting_conditions. 2003-07-04 Alexandre Duret-Lutz * src/tgbaalgos/ltl2tgba.cc (ltl_trad_visitor::visit): Declare accepting conditions w.r.t. to Now variables, not Next. 2003-07-03 Alexandre Duret-Lutz * src/tgba/tgbaproduct.cc (tgba_product_succ_iterator::first): Simplify, do not call next_non_false_() if 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.