1. 19 Aug, 2003 1 commit
  2. 18 Aug, 2003 3 commits
  3. 15 Aug, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      This implements Couvreur's FM'99 ltl2tgba translation. · 2b9f1720
      Alexandre Duret-Lutz authored
      * src/tgba/bdddict.cc (bdd_dict::is_registered): Split as ...
      (bdd_dict::is_registered_proposition, bdd_dict::is_registered_state,
      bdd_dict::is_registered_accepting_variable): ... these.
      * src/tgba/bdddict.hh: Likewise.
      * src/tgba/tgbaexplicit.cc (tgba_explicit::set_init_state): New method.
      (tgba_explicit::declare_accepting_condition): Arrange so that this
      function can be called during the construction of the automaton.
      (tgba_explicit::complement_all_accepting_conditions): New method.
      (tgba_explicit::has_accepting_condition): Adjust to call
      bdd_dict::is_registered_accepting_variable.
      * src/tgba/tgbaexplicit.hh (tgba_explicit::set_init_state,
      tgba_explicit::complement_all_accepting_conditions): New methods.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
      New files.
      * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
      libtgbaalgos_la_SOURCES): Add them.
      * src/tgbaalgos/ltl2tgba.hh: Add bibtex entry in comment.
      * src/tgbatest/Makefile.am (check_PROGRAMS): Remove spotlbtt
      and tbalbtt.
      (tbalbtt_SOURCES, tbalbtt_CXXFLAGS, spotlbtt_SOURCES): Remove.
      * src/tgbatest/spotlbtt.cc: Delete, superseded by "ltl2tgba -F -t".
      * src/tgbatest/ltl2tgba.cc: Implement the -f and -F options.
      * src/tgbatest/spotlbtt.test: Use "ltl2tgba -F -t" instead of
      "spotlbtt", "ltl2tgba -F -t -D" instead of "tbalbtt", and add
      also check the ltl2tgba_fm translator.
      * wrap/python/spot.i: Wrap ltl2tgba_fm.
      * wrap/python/cgi/ltl2tgba.in: Add radio buttons to select
      between ltl2tgba and ltl2tgba_fm.
      * wrap/python/tests/ltl2tgba.py: Add support for the -f option.
      * wrap/python/tests/ltl2tgba.test: Try the -f option.
      2b9f1720
    • Alexandre Duret-Lutz's avatar
      varnum can be augmented by other allocator. Keep track · 256d8005
      Alexandre Duret-Lutz authored
      of a local varnum (lvarnum) in each allocator.
      * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Initialize
      lvarnum.
      (bdd_allocator::extvarnum): New method.
      (bdd_allocator::allocate_variables): Use lvarnum and extvarnum.
      * src/misc/bddalloc.hh (bdd_allocator::extvarnum): New mathod.
      (bdd_allocator::lvarnum): New variable.
      256d8005
  4. 14 Aug, 2003 1 commit
  5. 11 Aug, 2003 1 commit
  6. 10 Aug, 2003 5 commits
  7. 08 Aug, 2003 1 commit
  8. 07 Aug, 2003 1 commit
  9. 06 Aug, 2003 8 commits
  10. 05 Aug, 2003 4 commits
  11. 04 Aug, 2003 6 commits
  12. 01 Aug, 2003 7 commits