1. 14 Apr, 2005 1 commit
  2. 20 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/sanity/style.test: Catch occurrences of "accepting condition". · a2cbe9ca
      Alexandre Duret-Lutz authored
      * bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh,
      src/sanity/style.test, src/tgba/bdddict.cc,
      src/tgba/succiterconcrete.hh, src/tgba/tgbabddcoredata.hh,
      src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbatest/dfs.test: Replace them by "acceptance condition".
      a2cbe9ca
  3. 18 Feb, 2005 3 commits
  4. 17 Feb, 2005 4 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc · 4e1916ec
      Alexandre Duret-Lutz authored
      (emptiness_check_instantiator): New class.
      * src/misc/optionmap.hh (set (const option_map&)): New method.
      * src/tgbatest/randtgba.cc: Create every emptiness check via
      emptiness_check_instantiator.
      4e1916ec
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness.hh, · 435b03c2
      Alexandre Duret-Lutz authored
      src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method.
      * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Implement it.
      * src/tgbatest/randtgba.cc: Simplify.
      435b03c2
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, · c1d0cab3
      Alexandre Duret-Lutz authored
      src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Provide wrapper
      functions that read the hash-map size from a "bsh" option.
      * src/tgbatest/randtgba.cc: Simplify.
      c1d0cab3
    • Alexandre Duret-Lutz's avatar
      * src/misc/optionmap.hh, src/misc/optionmap.cc · fed4b6f0
      Alexandre Duret-Lutz authored
      (option_map::parse_options): Rewrite.  Do not modify the input
      string, allow !foo as a shorthand for foo=0, and support K and
      M suffixes for values.
      * src/tgbatest/randtgba.cc (cons_emptiness_check): Simplify.
      * wrap/python/spot.i: Process optionmap.hh.
      * wrap/python/tests/optionmap.py: New file.
      * wrap/python/tests/Makefile.am (TESTS): Add it.
      fed4b6f0
  5. 16 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get, · f3effb9d
      Alexandre Duret-Lutz authored
      option_map::set): Handle default values.
      (anonymous::to_int): Do not print anything.
      * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in
      the constructor.
      * src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise.  Handle
      the "poprem", "group", and "shy" options via the option_map.
      Supply a couvreur99() wrapper to the shy/non-shy variant.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
      iface/gspn/ssp.cc: Adjust.
      f3effb9d
  6. 08 Feb, 2005 1 commit
  7. 07 Feb, 2005 1 commit
    • Denis Poitrenaud's avatar
      * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map): New class. · 661dee86
      Denis Poitrenaud authored
      * src/misc/Makefile.am: Add it.
      * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: Add option
      facilities to the classes emptiness_check and emptiness_result
      * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh: Compute optionnaly
      accepting runs from stack.
      * src/tgbatest/randtgba.cc: Make this option public.
      661dee86
  8. 04 Feb, 2005 1 commit
  9. 03 Feb, 2005 1 commit
    • Alexandre Duret-Lutz's avatar
      * tgbaalgos/emptiness_stats.hh (unsigned_statistics): New base · 9c2c3926
      Alexandre Duret-Lutz authored
      class for ec_statistics and ars_statistics.
      (acss_statistics): Inherit from ars_statistics.
      * tgbaalgos/emptiness.cc, tgbaalgos/emptiness.hh:
      (emptiness_check::statistics, emptiness_check_result::statistics):
      New methods.
      * tgbatest/randtgba.cc: Adjust to use the above.
      * tgbaalgos/gv04.cc, tgbaalgos/ndfs_result.hxx, tgbaalgos/gtec/ce.cc,
      tgbaalgos/gtec/ce.hh: Do not inherit from ars_statistics if
      acss_statistics is used.
      9c2c3926
  10. 02 Feb, 2005 2 commits
  11. 01 Feb, 2005 1 commit
  12. 31 Jan, 2005 1 commit
  13. 29 Jan, 2005 2 commits
  14. 28 Jan, 2005 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. · 5fb5b684
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy):
      Add the poprem option.
      * src/tgbaalgos/gtec/gtec.cc: Implement it.
      * src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh
      (scc_stack::rem, scc_stack::clear_rem,
      scc_stack::connected_component::rem): New.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants.
      5fb5b684
    • Denis Poitrenaud's avatar
      * src/tgbatest/dfs.test, src/tgbatest/emptchk.test, · b1800e38
      Denis Poitrenaud authored
      src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/tba_samples_from_spin.test:
      Adjust names of emptiness check algorithms.
      b1800e38
  15. 25 Jan, 2005 1 commit
  16. 24 Jan, 2005 3 commits
  17. 13 Jan, 2005 3 commits
  18. 12 Jan, 2005 1 commit
  19. 10 Jan, 2005 4 commits
  20. 03 Jan, 2005 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class. · 55c08790
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from
      ars_statistics.
      (ndfs_result::dfs): Call inc_ars_states().
      (ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics.
      * tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit
      from ars_statistics.
      * tgbaalgos/gtec/ce.cc (shortest_path,
      couvreur99_check_result::accepting_cycle::scc_bfs):
      Update ars_statistics.
      * src/tgbatest/randtgba.cc: Display statistics about accepting run
      search.
      55c08790
    • Alexandre Duret-Lutz's avatar
      * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. · ca2fe6c7
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh
      (couvreur99_check_result): Inherit from acss_statistics.
      (couvreur99_check_result::acss_states): Implement it.
      * src/tgbatest/randtgba.cc: Display statistics about accepting cycle
      search space.
      ca2fe6c7
  21. 16 Dec, 2004 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/randtgba.cc: Add option -O, so we can profile each · 58aff37d
      Alexandre Duret-Lutz authored
      emptiness-check on its own.
      58aff37d
    • Alexandre Duret-Lutz's avatar
      * src/ltlparse/ltlscan.ll: Pass yyleng to the std::string constructor, · 0efca0f6
      Alexandre Duret-Lutz authored
      so it doesn't have to compute it.
      * src/tgbaparse/tgbascan.ll: Likewise.
      (YY_USER_INIT, current_file): Remove, it is too costly to use
      yy::Location::filename in the current implementation
      of yy::Location (this attribute is duplicated for each token).
      Leaving it empty divides the parsing time by 3.
      * src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh
      (format_tgba_parse_errors): Take the filename as argument.
      * src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
      src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
      iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls
      to format_tgba_parse_errors.
      0efca0f6
  22. 14 Dec, 2004 1 commit
  23. 10 Dec, 2004 1 commit