1. 22 Apr, 2004 2 commits
  2. 21 Apr, 2004 8 commits
  3. 20 Apr, 2004 2 commits
  4. 17 Apr, 2004 2 commits
  5. 15 Apr, 2004 3 commits
    • Alexandre Duret-Lutz's avatar
      Rename EESRG as SSP. · 133bcf94
      Alexandre Duret-Lutz authored
      * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
      iface/gspn/dottyeesrg.cc: Rename as ...
      * iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc:
      ... these.  Adjust all classes and function names.
      * iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes
      filenames and function names.
      * m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS.
      133bcf94
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): · 8ff4ca08
      Alexandre Duret-Lutz authored
      Rewrite.
      (numbered_state_heap_hash_map::index): New functions.
      (numbered_state_heap_hash_map::filter): Delete.
      * src/tgbaalgos/gtec/nsheap.hh
      (numbered_state_heap_hash_map::index): New functions.
      (numbered_state_heap_hash_map::filter): Delete.
      * iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find,
      numbered_state_heap_eesrg_semi::index): Rewrite.
      (numbered_state_heap_eesrg_semi::filter): Remove.
      * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc:
      Adjust to use find() and index() instead of filter()..
      8ff4ca08
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): · be4f4e33
      Alexandre Duret-Lutz authored
      Free filtered states.
      (emptiness_check_shy_eesrg): New class.
      (emptiness_check_eesrg_shy): New function.
      * iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function.
      * iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5.
      * * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc
      (emptiness_check_shy::check): Move arc, num, succ_queue, and todo
      as attributes.
      (emptiness_check_shy::find_state): New virtual function.
      be4f4e33
  6. 14 Apr, 2004 4 commits
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/ltlgspn.cc (connected_component_eesrg, · 1e360ec6
      Alexandre Duret-Lutz authored
      connected_component_eesrg_factory, numbered_state_heap_eesrg_semi,
      numbered_state_heap_eesrg_const_iterator,
      numbered_state_heap_eesrg_factory_semi): New classes.
      (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi,
      counter_example_eesrg): New functions.
      * iface/gspn/eesrg.hh (emptiness_check_eesrg_semi,
      emptiness_check_eesrg_shy_semi, counter_example_eesrg): New
      functions.
      * iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions.
      1e360ec6
    • Alexandre Duret-Lutz's avatar
      * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg, · 5d4affc5
      Alexandre Duret-Lutz authored
      state_gspn_eesrg): Compute the array of all successors of the
      right state beforehand, pass it to Greatspn (left automata) at
      once, let it compute the resulting synchronized arcs, and iterate
      on that result.
      5d4affc5
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory, · a2cd1de2
      Alexandre Duret-Lutz authored
      numbered_state_heap_hash_map_factory): New class.
      * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory):
      Implement it.
      * src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check,
      emptiness_check_shy::emptiness_check_shy): Take a
      numbered_state_heap_factory argument.
      * tgbaalgos/gtec/status.hh
      (emptiness_check_status::emptiness_check_status): Likewise.
      (emptiness_check_status::h): Make it a numbered_state_heap*.
      * src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc,
      tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h.
      a2cd1de2
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: · 579c343e
      Alexandre Duret-Lutz authored
      Delete and split into ...
      * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
      src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
      src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
      src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
      these new files.
      * src/tgbaalgos/gtec/Makefile.am: New file.
      * src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
      Recurse into gtec and link gtec/libgtec.la.
      (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
      and emptinesscheck.cc.
      * configure.ac: Output src/tgbalagos/gtec/Makefile.
      * iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
      * README: Update tree description.
      579c343e
  7. 13 Apr, 2004 10 commits
  8. 05 Apr, 2004 1 commit
  9. 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
  10. 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
  11. 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
  12. 09 Mar, 2004 1 commit
  13. 08 Mar, 2004 2 commits