1. 04 May, 2004 2 commits
  2. 03 May, 2004 1 commit
  3. 23 Apr, 2004 4 commits
  4. 22 Apr, 2004 2 commits
  5. 21 Apr, 2004 8 commits
  6. 20 Apr, 2004 2 commits
  7. 17 Apr, 2004 2 commits
  8. 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
  9. 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
  10. 13 Apr, 2004 10 commits
  11. 05 Apr, 2004 1 commit
  12. 25 Mar, 2004 1 commit
    • 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