1. 13 Apr, 2004 3 commits
  2. 05 Apr, 2004 1 commit
  3. 25 Mar, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var · fa6ac39c
      Alexandre Duret-Lutz authored
      variables from a shared bdd_dict.  Register Next variables as
      anonymous variables.
      (translate_dict::translate_dict, translate_dict::~translate_dict,
      translate_dict::register_proposition,
      translate_dict::register_a_variable,
      translate_dict::register_next_variable,
      translate_dict::dump, translate_dict::var_to_formula,
      ltl_to_tgba_fm): Adjust.
      (translate_dict::dict): New attribute.
      (translate_dict::a_map, translate_dict::a_formula_map,
      translate_dict::var_map, translate_dict::var_formula_map): Delete.
      fa6ac39c
    • Alexandre Duret-Lutz's avatar
      * src/misc/freelist.cc (free_list::remove): Work around · 3c3b23bf
      Alexandre Duret-Lutz authored
      invalidated iterators.
      * tgba/bdddict.cc (unregister_variable): New methods,
      extracted from ...
      (bdd_dict::unregister_all_my_variables): ... here.
      * tgba/bdddict.hh (unregister_variable): Declare them.
      3c3b23bf
  4. 23 Mar, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/misc/freelist.hh (free_list::remove, free_list::insert): New · 784ccafb
      Alexandre Duret-Lutz authored
      methods.
      * src/misc/freelist.cc (free_list::register_n,
      free_list::releases_n): Rewrite using free_list::remove and
      free_list::insert.
      (free_list::remove, free_list::insert): New methods.
      * src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables):
      New method.
      (bdd_dict::annon_free_list): New subclass.
      (bdd_dict::free_annonymous_list_of_type_of): New attribute.
      * src/tgba/bdddict.cc (bdd_dict::register_all_variables_of,
      bdd_dict::unregister_all_my_variables): Handle anonymous variables
      too.
      (bdd_dict::register_anonymous_variables,
      bdd_dict::annon_free_list::annon_free_list,
      bdd_dict::annon_free_list::extend): New methods.
      784ccafb
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path) · aba2dc75
      Alexandre Duret-Lutz authored
      Fix handling of PATH when backtracking.  Report from Soheib Baarir.
      aba2dc75
  5. 18 Mar, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      Move the free_list management into a separate class for reuse. · cf6602a3
      Alexandre Duret-Lutz authored
      * src/misc/freelist.hh, src/misc/freelist.cc: New files.
      * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
      * src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
      make dump_free_list visible.
      * src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
      all the code into free_list::register_n() and
      bdd_allocator::extend(), and call the former.
      (bdd_allocator::release_variables): Move all the code into
      free_list::release_n() and call it.
      (bdd_allocator::extend): New method.
      * src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;
      cf6602a3
  6. 09 Mar, 2004 1 commit
  7. 08 Mar, 2004 5 commits
  8. 21 Feb, 2004 2 commits
  9. 20 Feb, 2004 5 commits
  10. 19 Feb, 2004 2 commits
  11. 16 Feb, 2004 4 commits
  12. 13 Feb, 2004 1 commit
  13. 12 Feb, 2004 1 commit
  14. 11 Feb, 2004 2 commits
  15. 10 Feb, 2004 2 commits
  16. 09 Feb, 2004 2 commits
  17. 08 Feb, 2004 1 commit
    • Alexandre Duret-Lutz's avatar
      This should help getting accurate statistics (on both the · 7069d540
      Alexandre Duret-Lutz authored
      formula automaton and the synchronized product) from LBTT.
      Idea from Jean-Michel Couvreur.
      
      * src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
      (nonacceptant_lbtt_reachable): New function.
      * src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
      function.
      * src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
      if the -T option is used.
      * src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
      default.
      7069d540
  18. 05 Feb, 2004 2 commits
  19. 04 Feb, 2004 1 commit