1. 28 May, 2009 1 commit
  2. 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
  3. 09 Apr, 2009 1 commit
    • Guillaume Sadegh's avatar
      Minor fixes to compile with GCC 4.4. · bbbc1acc
      Guillaume Sadegh authored
      2009-04-09  Guillaume SADEGH  <sadegh@lrde.epita.fr>
      
      	* src/eltlparse/eltlparse.yy (subformula): Avoid a comparaison
      	between a signed and an unsigned value.
      	* src/ltlast/automatop.hh, src/ltlast/automatop.cc (nfa): Avoid
      	a name clash with the `nfa' class.
      bbbc1acc
  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 5 commits
  8. 23 Feb, 2009 2 commits
  9. 18 Feb, 2009 1 commit
  10. 19 Dec, 2008 1 commit
  11. 18 Dec, 2008 1 commit
  12. 11 Dec, 2008 2 commits
  13. 10 Dec, 2008 2 commits
  14. 02 Dec, 2008 1 commit
  15. 29 Aug, 2008 3 commits
  16. 27 Aug, 2008 2 commits
  17. 26 Aug, 2008 3 commits
  18. 08 Aug, 2008 1 commit
  19. 07 Aug, 2008 1 commit
  20. 20 Jun, 2008 1 commit
  21. 12 Jun, 2008 4 commits
  22. 11 Jun, 2008 4 commits