1. 09 Nov, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Deprecate ltl::destroy(f) in favor of f->destroy() · 77df39b4
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
      Transform this static function into a member function.
      * src/ltlvisit/destroy.hh (destroy): Document and declare as
      deprecated.
      * bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
      src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
      src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
      src/ltlast/automatop.cc, src/ltlast/binop.cc,
      src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
      src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/readltl.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
      src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
      src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
      src/tgba/bddprint.cc, src/tgba/taa.cc,
      src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
      src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
      src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
      wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
      the #include "destroy.hh" when appropriate.
      77df39b4
    • Alexandre Duret-Lutz's avatar
      Add missing instance_count() in automatop and eltl2tgba. · f2e941cd
      Alexandre Duret-Lutz authored
      * src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing
      instance_count() functions.
      * src/tgbatests/eltl2tgba.cc: Add missing instance_count()
      assertions at the end.
      * src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(),
      even if automatop are not used in ltl2tgba yet.  This way we won't
      forget once eltl2tgba and ltl2tgba are merged.
      f2e941cd
  2. 07 Sep, 2009 1 commit
    • Damien Lefortier's avatar
      Add an algorithm (from Couvreur) working on BDDs to reduce the · edd4b2b5
      Damien Lefortier authored
      size of TGBAs represented as BDDs by deleting unaccepting SCCs.
      
      * src/eltlparse/eltlparse.yy: Remove a warning.
      * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
      new function delete_unaccepting_scc in both classes.
      * src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
      new function in LaCIM for ELTL and bench it.
      * src/tgbatest/defs.in: Fix it.
      * bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
      ELTL in benchs.
      edd4b2b5
  3. 26 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Extend the ELTL parser to support more complex aliases of · b06c9cd5
      Damien Lefortier authored
      automaton operators such as Strong=G(F($0))->G(F($1)) and
      G=R(false, $0).
      
      * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add
      support for more complex aliases.
      * src/eltltest/acc.cc, src/eltltest/acc.test: Adjust.
      * src/ltlast/nfa.cc, src/ltlast/nfa.hh (arity): Now returns an
      unsigned value.
      * src/tgbatest/eltl2tgba.test: Adjust.
      * src/tgbalagos/eltl2tgba_lacim.cc: Fix sanity.
      b06c9cd5
  4. 08 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Correct LaCIM for ELTL and make it work with LBTT. · 7643c49c
      Damien Lefortier authored
      * src/eltlparse/eltlparse.yy: Adjust.
      * src/ltlast/automatop.cc, src/ltlast/automatop.hh,
      src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc: Clean the way we
      handle the negation of automaton operators.
      * src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Add an
      optional argument to output a fully parenthesized string.
      * src/tgbaalgos/eltl2tgba_lacim.cc: Fix it.
      * src/tgbatest/eltl2tgba.cc: Add a new option (-L) to read formulae
      from an LBTT-compatible file.
      * src/tgbatest/eltl2tgba.test: A new tests.
      * src/tgbatest/spotlbtt.test: Add LaCIM for ELTL.
      7643c49c
  5. 04 Apr, 2009 1 commit
    • Damien Lefortier's avatar
      Extend the ELTL parser to support basic aliases of automaton · 355461ae
      Damien Lefortier authored
      operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix
      notation for binary automaton operators.
      
      * README: Document the ELTL directories.
      * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add
      support for aliases and infix notation.
      * src/eltlparse/public.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh:
      Clean them.
      * src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Add tests
      for the ELTL parser's extensions.
      * src/tgbatest/eltl2tgba.cc: Adjust.
      355461ae
  6. 26 Mar, 2009 1 commit
    • Damien Lefortier's avatar
      Add support for ELTL (AST & parser), and an adaptation of LaCIM · 2fbcd7e5
      Damien Lefortier authored
      for ELTL.  This is a new version of the work started in 2008 with
      LTL and ELTL formulae now sharing the same class hierarchy.
      
      * configure.ac: Adjust for src/eltlparse/ and src/eltltest/
      directories, and call AX_BOOST_BASE.
      * m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]).
      * src/Makefile.am: Add eltlparse and eltltest.
      * src/eltlparse/: New directory.  Contains the ELTL parser.
      * src/eltltest/: New directory.  Contains tests related to
      ELTL (parser and AST).
      * src/ltlast/Makefile.am: Adjust for ELTL AST files.
      * src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files.
      Represent automaton operators nodes used in ELTL ASTs.
      * src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files.  Represent
      simple NFAs used internally by automatop nodes.
      * src/ltlast/allnode.hh, src/ltlast/predecl.hh,
      src/ltlast/visitor.hh: Adjust for automatop.
      * src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/dotty.cc, src/ltlvisit/nenoform.cc,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
      src/ltlvisit/tostring.cc: Because LTL and ELTL formulae share the
      same class hierarchy, LTL visitors need to handle automatop nodes
      to compile.  When it's meaningful the visitor applies on automatop
      nodes or simply assert(0) otherwise.
      * src/tgba/tgbabddconcretefactory.cc (create_anonymous_state),
      src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New
      function used by the LaCIM translation algorithm for ELTL.
      * src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files.
      * src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/eltl2tgba_lacim.hh: New files.  Implementation of
      the LaCIM translation algorithm for ELTL.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
      Handle automatop nodes in the translation by an assert(0).
      * src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files.
      * src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New
      files
      2fbcd7e5
  7. 25 Mar, 2009 1 commit
  8. 20 Jun, 2008 1 commit
  9. 17 Apr, 2008 1 commit
  10. 25 Feb, 2008 1 commit
  11. 17 Nov, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, · 36aadba7
      Alexandre Duret-Lutz authored
      src/ltlast/constant.hh, src/ltlast/formula.hh,
      src/ltlast/multop.hh, src/ltlast/refformula.hh,
      src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh,
      src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
      src/ltlparse/public.hh, src/ltlvisit/apcollect.hh,
      src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
      src/ltlvisit/dump.hh, src/ltlvisit/length.hh,
      src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen
      groups for LTL algorithms and types.
      * doc/Makefile.am (fast-doc): New target.
      36aadba7
  12. 21 Nov, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * COPYING: New file. · 43a91a15
      Alexandre Duret-Lutz authored
      * Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
      iface/gspn/Makefile.am, iface/gspn/common.cc,
      iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
      iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
      iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
      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/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
      src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltltest/Makefile.am,
      src/ltltest/defs.in, src/ltltest/equals.cc,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc, src/ltltest/tostring.test,
      src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
      src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
      src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
      src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
      src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
      src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.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/tgba.cc, 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/tgbabddfactory.hh,
      src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
      src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
      src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
      src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
      src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, 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/Makefile.am,
      src/tgbatest/bddprod.test, src/tgbatest/defs.in,
      src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
      wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
      wrap/python/spot.i, wrap/python/cgi/Makefile.am,
      wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
      wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
      wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/run.in: Add Copyright license.
      43a91a15
  13. 01 Aug, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: Merge the · f1f81fbf
      Alexandre Duret-Lutz authored
      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.
      f1f81fbf
  14. 06 Jun, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/clone.cc (clone): New const version. · 3991a51a
      Alexandre Duret-Lutz authored
      * 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.
      3991a51a
  15. 15 May, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Implements spot::ltl::destroy() and exercise it. · 9123e56f
      Alexandre Duret-Lutz authored
      * 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.
      9123e56f