1. 09 Nov, 2009 2 commits
    • Alexandre Duret-Lutz's avatar
      Better types for instance maps. · 3488bf45
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.hh (map): Use unop* as values.
      * src/ltlast/binop.hh (map): Use binop* as values.
      * src/ltlast/multop.hh (map): Use multop* as values.
      * src/ltlast/automatop.hh (paircmp): Rename as tripletcmp.
      (map): Use automaton* as values, not formula*.
      3488bf45
    • 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 Nov, 2009 2 commits
  3. 05 Nov, 2009 2 commits
  4. 04 Nov, 2009 2 commits
  5. 03 Nov, 2009 1 commit
  6. 28 Oct, 2009 2 commits
  7. 23 Oct, 2009 1 commit
  8. 22 Oct, 2009 3 commits
    • Alexandre Duret-Lutz's avatar
      Escape labels in -KV output. · 913637a7
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.cc (dump_scc_dot): Escape labels and other
      strings output between quote in dot.
      * src/tgbatest/kv.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      913637a7
    • Alexandre Duret-Lutz's avatar
      4d8239e8
    • Damien Lefortier's avatar
      Improve ltl_to_taa. · 7ce27ef9
      Damien Lefortier authored
      * src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not
      on-the-fly anymore allowing some redundant transitions to be
      removed. Also a new function to output a TAA.
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the
      refined rules from Tauriainen.
      * src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in
      ltl_to_taa.
      * src/tgbatest/spotlbtt.test: More tests.
      7ce27ef9
  9. 17 Oct, 2009 1 commit
  10. 16 Oct, 2009 3 commits
    • Damien Lefortier's avatar
      Minor fixes. · 84060b49
      Damien Lefortier authored
      * src/misc/bddop.hh, src/tgba/taa.hh, src/tgbaalgos/ltl2taa.hh:
      Fix sanity (incorrect include guard).
      * src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh:
      Copyright 2009.
      * src/tgbaalgos/eltl2tgba_lacim.cc: Use abbreviations.
      * src/tgbatest/taa.cc: Fix it.
      84060b49
    • Damien Lefortier's avatar
      Add a new algorithm (from Tauriainen) to translate LTL formulae to · 627b6677
      Damien Lefortier authored
      TGBA which uses TAA as an intermediate representation.  This is a
      basic version, optimizations and enhancements will come later.
      
      * src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: The algortihm.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba: New option: -taa, which uses this new
      translation algorithm.
      * src/tgbatest/spotlbtt.test: Add ltl2tgba -taa.
      627b6677
    • Damien Lefortier's avatar
      Add a class to represent Transition-based Alternating Automata (TAA). · 20c1f01e
      Damien Lefortier authored
      * misc/Makefile.am, misc/bbop.cc, misc/bddop.hh: Factorize some
      code on BDDs to compute all_acceptance_conditions from
      neg_acceptance_condition.
      * src/tgba/Makefile.am, src/tgbatest/Makefile.am: Adjust.
      * src/tgba/taa.cc, src/tgba/taa.hh: The TAA class.
      * src/tgba/tgbaexplicit.hh: Use the factorized code in bddop.hh.
      * src/tgbatest/taa.cc, src/tgbatest/taa.test: Some test cases.
      20c1f01e
  11. 07 Oct, 2009 1 commit
  12. 01 Oct, 2009 7 commits
  13. 28 Sep, 2009 1 commit
  14. 18 Sep, 2009 1 commit
    • Alexandre Duret-Lutz's avatar
      Optimize previous patch. · fd0de04d
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/scc.hh (scc_map::scc::supp_rec): Initialize to
      bddfalse, since this cannot occur in reallife.
      * src/tgbaalgos/scc.cc (scc_map::update_supp_rec): Adjust.
      fd0de04d
  15. 17 Sep, 2009 2 commits
  16. 08 Sep, 2009 1 commit
  17. 07 Sep, 2009 4 commits
    • Damien Lefortier's avatar
      Fix some memory leaks. · 99533561
      Damien Lefortier authored
      * src/eltlparse/eltlparse.yy: Free the automatop::vec when
      CHECK_ARITY fails while parsing an automatop.
      * src/eltltest/acc.cc: Free all constructed formulae.
      99533561
    • Alexandre Duret-Lutz's avatar
      Fix a memory leak in reduce_tau03(). · 4964c9a1
      Alexandre Duret-Lutz authored
      * src/ltlvisit/contain.cc (reduce_tau03_visitor::visit): Free
      the operand array when a multop reduces to a constant.
      4964c9a1
    • Alexandre Duret-Lutz's avatar
      Fix a memory leak in randltl. · 058bb83c
      Alexandre Duret-Lutz authored
      * src/ltltest/randltl.cc: Free the atomic properties from AP
      before exit.
      058bb83c
    • 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
  18. 02 Sep, 2009 4 commits
    • Alexandre Duret-Lutz's avatar
      Fix path to libtool in test suites. · dc8cb56b
      Alexandre Duret-Lutz authored
      * src/ltltest/defs.in, src/eltltest/defs.in, src/tgbatest/defs.in,
      src/evtgbatest/defs.in (run): Use ../../../libtool instead of
      ../../libtool, now that testcases have been moved down one directory.
      dc8cb56b
    • Alexandre Duret-Lutz's avatar
      Use Automake 1.11's parallel-tests feature. · 1098c62d
      Alexandre Duret-Lutz authored
      * configure.ac: Enable parallel-tests.
      * src/eltltest/defs.in, src/evtgbatest/defs.in,
      src/ltltest/defs.in, src/tgbatest/defs.in: Always output verbose
      tests.  Make a subdirectory for each test case.
      * src/ltltest/Makefile.am, src/eltltest/Makefile.am,
      src/tgbatest/Makefile.am, src/evtgbatest/Makefile.am: Remove
      CLEANFILES and clean the test subdirectories in a distclean-local
      rule instead.
      * src/eltltest/acc.test, src/eltltest/nfa.test,
      src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.test,
      src/evtgbatest/product.test, src/evtgbatest/readsave.test,
      src/ltltest/equals.test, src/ltltest/lunabbrev.test,
      src/ltltest/nenoform.test, src/ltltest/parse.test,
      src/ltltest/parseerr.test, src/ltltest/reduc.test,
      src/ltltest/reduccmp.test, src/ltltest/syntimpl.test,
      src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
      src/ltltest/tunenoform.test, src/tgbatest/bddprod.test,
      src/tgbatest/complementation.test, src/tgbatest/dfs.test,
      src/tgbatest/dupexp.test, src/tgbatest/eltl2tgba.test,
      src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
      src/tgbatest/emptchkr.test, src/tgbatest/explicit.test,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
      src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.test,
      src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
      src/tgbatest/readsave.test, src/tgbatest/reduccmp.test,
      src/tgbatest/reductgba.test, src/tgbatest/scc.test,
      src/tgbatest/spotlbtt.test, src/tgbatest/tgbaread.test,
      src/tgbatest/tripprod.test: Adjust to run from a subdirectory.
      1098c62d
    • Alexandre Duret-Lutz's avatar
      more files to ignore · 1f7aa90d
      Alexandre Duret-Lutz authored
      1f7aa90d
    • Alexandre Duret-Lutz's avatar