- 20 Feb, 2005 2 commits
-
-
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".
-
Alexandre Duret-Lutz authored
misc/optionmap.hh.
-
- 18 Feb, 2005 4 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
"condition heuristic". Suggested by Heikki Tauriainen. * src/tgbatest/randtgba.cc: Test it.
-
Alexandre Duret-Lutz authored
all algorithms from a file. Use the emptiness_check_instantiator syntax as name in the output. * bench/emptchk/defs.in: DEfine ALGORITHMS here. * bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh, bench/emptchk/pml-clserv.sh: Use $ALGORITHMS. * src/misc/timer.cc: Truncate long keys in display.
-
Alexandre Duret-Lutz authored
emptiness_check_instantiator. * src/tgba/tgba.cc, src/tgba/tgba.hh (tgba::number_of_acceptance_conditions): Return an unsigned. * bench/emptchk/algorithms, bench/emptchk/README, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust references to algorithms. * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote variables properly.
-
- 17 Feb, 2005 4 commits
-
-
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.
-
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.
-
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.
-
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.
-
- 16 Feb, 2005 1 commit
-
-
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.
-
- 08 Feb, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
unsigned_statistics interface. * bench/emptchk/README: Adjust description of output.
-
- 07 Feb, 2005 3 commits
-
-
Alexandre Duret-Lutz authored
file, so that strings are not checked for our C++ style. Reported by Denis (with a chainsaw).
-
Denis Poitrenaud authored
-
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.
-
- 05 Feb, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 04 Feb, 2005 4 commits
-
-
Alexandre Duret-Lutz authored
(ec_stat, acss_stat, ars_stat, print_ec_stats, print_acss_stats, print_ars_stats): ... these. * tgbaalgos/emptiness_stats.hh (unsigned_statistics): Make the map public.
-
Alexandre Duret-Lutz authored
Use char_ptr_less_than.
-
Alexandre Duret-Lutz authored
* src/misc/Makefile.am (misc_HEADERS): Add it.
-
Alexandre Duret-Lutz authored
Use char* for keys, not std::string.
-
- 03 Feb, 2005 2 commits
-
-
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.
-
Alexandre Duret-Lutz authored
-
- 02 Feb, 2005 3 commits
-
-
Alexandre Duret-Lutz authored
* src/tgbatest/randtgba.cc: Check the range of all arguments.
-
Alexandre Duret-Lutz authored
* bench/emptchk/Makefile.am: Distribute models/eeaean1.pml and build models/eeaean1.tgba. * bench/emptchk/pml-eeaean.sh: Check models/eeaean1.pml. * bench/emptchk/README: Adjust. * bench/emptchk/defs.in (RANDTGBA, LTL2TGBA): These tools are in the build tree, not the source tree...
-
Alexandre Duret-Lutz authored
and by bench/emptchk/. * src/tgbatest/tba_samples_from_spin.test: Delete. * src/tgbatest/tba_samples_from_spin/: Delete. * src/tgbatest/Makefile.am: Adjust.
-
- 01 Feb, 2005 4 commits
-
-
Alexandre Duret-Lutz authored
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/evtgbatest/product.cc, src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update to Bison 2.0.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
(syntax): Categorize options.
-
- 31 Jan, 2005 3 commits
-
-
Alexandre Duret-Lutz authored
src/tgbatest/explprod.test, src/tgbatest/tripprod.test, src/evtgbatest/explicit.test: Do not reorder the output. It's pointless since 2005-01-20.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
- 30 Jan, 2005 1 commit
-
-
Alexandre Duret-Lutz authored
and pml-eeaean.sh. * bench/emptchk/ltl-human.sh: Typo in densities. Reported by Denis.
-
- 29 Jan, 2005 7 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
message if -0 is used.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
-
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.
-