2003-06-05 Alexandre Duret-Lutz * 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.