317 lines
13 KiB
Text
317 lines
13 KiB
Text
2003-05-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
|
|
|
|
Check trivial multop equality at build time. The 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 <aduret@src.lip6.fr>
|
|
|
|
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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <rebiha@nyx>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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 <aduret@src.lip6.fr>
|
|
|
|
* 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.
|