Commit graph

alarsyo/spot

Fork 0

ecaedbba4c * src/ltlvisit/length.cc (length_visitor): Rewrite using postfix_visitor. Alexandre Duret-Lutz 2005-02-23 00:35:45 +00:00
dd1bc78786 * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Add options "weights" and "redweights" (on by default). Alexandre Duret-Lutz 2005-02-22 17:37:33 +00:00
fa9614e997 * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Do not account for the size of condition_stack. Alexandre Duret-Lutz 2005-02-22 13:43:47 +00:00
a2cbe9cab8 * src/sanity/style.test: Catch occurrences of "accepting condition". * 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 2005-02-20 22:41:11 +00:00
7bbe3f5573 * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03.hh: Include misc/optionmap.hh. Alexandre Duret-Lutz 2005-02-20 22:19:15 +00:00
89c33952c9 * bench/emptchk/README: Document the file `algorithms'. Alexandre Duret-Lutz 2005-02-18 14:34:17 +00:00
ff8fe6802b * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Implement the "condition heuristic". Suggested by Heikki Tauriainen. * src/tgbatest/randtgba.cc: Test it. Alexandre Duret-Lutz 2005-02-18 14:13:26 +00:00
6314b682ba * src/tgbatest/randtgba.cc: Remplace the -O option by -A, reading 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 2005-02-18 12:28:42 +00:00
3b3a196526 * src/tgbatest/ltl2tgba.cc: Simplify using 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. Alexandre Duret-Lutz 2005-02-18 10:03:01 +00:00
4e1916ec50 * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc (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 2005-02-17 19:14:03 +00:00
435b03c2b2 * src/tgbaalgos/emptiness.hh, 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 2005-02-17 16:48:35 +00:00
c1d0cab3af * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, 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 2005-02-17 16:09:56 +00:00
fed4b6f05c * src/misc/optionmap.hh, src/misc/optionmap.cc (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. Alexandre Duret-Lutz 2005-02-17 15:01:51 +00:00
f3effb9da0 * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get, 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. Alexandre Duret-Lutz 2005-02-16 18:53:18 +00:00
77888e9293 * src/tgbatest/randtgba.cc: Factorize more code using the unsigned_statistics interface. * bench/emptchk/README: Adjust description of output. Alexandre Duret-Lutz 2005-02-08 18:33:14 +00:00
5cceccca06 * src/sanity/style.test: Strip all strings before checking the file, so that strings are not checked for our C++ style. Reported by Denis (with a chainsaw). Alexandre Duret-Lutz 2005-02-07 15:56:35 +00:00
b10727f139 * src/misc/optionmap.cc, src/misc/optionmap.hh: Typo (Hummm). Denis Poitrenaud 2005-02-07 15:47:36 +00:00
661dee8633 * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map): New class. * 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. Denis Poitrenaud 2005-02-07 15:18:41 +00:00
e812e1926f * src/misc/ltstr.hh: Include <functional> Alexandre Duret-Lutz 2005-02-05 10:18:31 +00:00
a5e9fb9df4 * src/tgbatest/randtgba.cc (stat_collector): New class, replacing... (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 2005-02-04 17:47:05 +00:00
081bdad5b4 * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): Use char_ptr_less_than. Alexandre Duret-Lutz 2005-02-04 16:16:05 +00:00
117aaf6772 * src/misc/ltstr.hh: New file. * src/misc/Makefile.am (misc_HEADERS): Add it. Alexandre Duret-Lutz 2005-02-04 15:27:24 +00:00
479c4833e0 * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): Use char* for keys, not std::string. Alexandre Duret-Lutz 2005-02-04 11:55:45 +00:00
9c2c3926c7 * tgbaalgos/emptiness_stats.hh (unsigned_statistics): New base 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 2005-02-03 17:37:11 +00:00
ad9eec60f1 * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Add pseudo code. Alexandre Duret-Lutz 2005-02-03 14:40:14 +00:00
5533e9dc35 * src/tgbaalgos/randomgraph.cc (random_graph): Make sure n > 0. * src/tgbatest/randtgba.cc: Check the range of all arguments. Alexandre Duret-Lutz 2005-02-02 16:03:31 +00:00
f22b59bf95 * bench/emptchk/models/eeaean1.pml: New file, from schwoon.05.tacas. * 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 2005-02-02 12:58:08 +00:00
2b68284dba These tests are huge, and are obsoleted by randtgba-based checks, and by bench/emptchk/. * src/tgbatest/tba_samples_from_spin.test: Delete. * src/tgbatest/tba_samples_from_spin/: Delete. * src/tgbatest/Makefile.am: Adjust. Alexandre Duret-Lutz 2005-02-02 10:30:39 +00:00
5cd58f9aaf * src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, 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 2005-02-01 18:03:00 +00:00
461fcd3732 * bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis. Alexandre Duret-Lutz 2005-02-01 16:52:22 +00:00
ce871f2f2e * bench/emptchk/README: Timing info from Denis. Alexandre Duret-Lutz 2005-02-01 13:23:34 +00:00
516350ddc0 * src/tgbatest/randtgba.cc (main): Skip empty lines. (syntax): Categorize options. Alexandre Duret-Lutz 2005-02-01 13:19:11 +00:00
42cd2e05b5 * src/tgbatest/explicit.test, src/tgbatest/explpro2.test, 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 2005-01-31 17:24:42 +00:00
885097ae62 * configure.ac, NEWS: Bump version to 0.1a. Alexandre Duret-Lutz 2005-01-31 13:01:08 +00:00
f07aba5ac3 * configure.ac, NEWS: Bump version to 0.1. Alexandre Duret-Lutz 2005-01-31 12:54:47 +00:00
db6973aaa8 * bench/emptchk/Makefile.am (dist_noinst_SCRIPTS): Add pml-clserv.sh and pml-eeaean.sh. * bench/emptchk/ltl-human.sh: Typo in densities. Reported by Denis. Alexandre Duret-Lutz 2005-01-30 10:18:24 +00:00
9e7138d9ab * doc/mainpage.dox: More text, and a link to "Modules". Alexandre Duret-Lutz 2005-01-29 16:47:01 +00:00
5c6471daca * src/tgbatest/ltl2tgba.cc (main): Silence the "filename.tgba read" message if -0 is used. Alexandre Duret-Lutz 2005-01-29 16:05:28 +00:00
cddca67fda * bench/emptchk/formulae.ltl: New file. Alexandre Duret-Lutz 2005-01-29 00:13:58 +00:00
de472c74b4 * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Document poprem. Alexandre Duret-Lutz 2005-01-29 00:07:21 +00:00
29548f695d * bench/emptchk/README: Make clearer that spin is needed. Alexandre Duret-Lutz 2005-01-29 00:00:06 +00:00
c8a9c2d48a * src/tgbatest/randtgba.cc (syntax): Missing std::endl. Alexandre Duret-Lutz 2005-01-28 23:57:41 +00:00
7bba6dc63d * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. * 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. Alexandre Duret-Lutz 2005-01-28 23:55:33 +00:00
5fb5b68407 * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. * 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. Alexandre Duret-Lutz 2005-01-28 17:17:54 +00:00
b1800e382c * src/tgbatest/dfs.test, src/tgbatest/emptchk.test, 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. Denis Poitrenaud 2005-01-28 15:57:52 +00:00
40ce79c733 * src/tgbaalgos/gtec/gtec.cc: Adjust statistics count to match how the algorithm will behave once remove_component() is revamped. From Alexandre. Denis Poitrenaud 2005-01-27 13:46:18 +00:00
311e1ba759 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_cycle): More ref in comment. Alexandre Duret-Lutz 2005-01-27 12:35:33 +00:00
acead199f5 * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/gtec/ce.cc: Do not account for states that are computed but not visited by the BFS&DFS used to construct accepting runs. Alexandre Duret-Lutz 2005-01-26 17:31:21 +00:00
68c0aa2e38 * src/tgbatest/randtgba.cc: Complete performance measurements. Denis Poitrenaud 2005-01-25 12:31:05 +00:00
1072b2dd99 * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/se05.hh: Correct pseudo-code. From Denis. Alexandre Duret-Lutz 2005-01-24 18:57:08 +00:00
42bc594193 * src/tgbaalgos/gtec/gtec.cc: Fake statistics count to match how the algorithm will behave once remove_component() is revamped. Alexandre Duret-Lutz 2005-01-24 15:25:56 +00:00
8f0135ebb0 * src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish states visited to compute the prefix and those for the cycle. * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/gtec/ce.cc: Adjust. * src/tgbatest/randtgba.cc: Print both statistics. Alexandre Duret-Lutz 2005-01-24 15:21:41 +00:00
f56abf58b8 * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add options Denis Poitrenaud 2005-01-24 14:41:27 +00:00
7d0b3fe297 * src/tgbatest/randtgba.cc: Some fixes from Denis for ratio stats. Alexandre Duret-Lutz 2005-01-24 14:35:44 +00:00
55cc650bfe * src/ltlast/formula.hh (formula_ptr_less_than): Two formulae with the same hash key are not necessary equal! Alexandre Duret-Lutz 2005-01-20 21:35:10 +00:00
5069a565b6 * src/ltlast/formula.hh (hash, dump, dump_, hash_key_): New members. (formula_ptr_less_than, formula_ptr_hash): New class. * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc, src/ltlast/multop.cc, src/ltlast/unop.cc: Adjust to handle dump_. * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: Sort the set using formula_ptr_less_than. * src/ltlvisit/dump.cc: Simplify using ->dump(). * src/tgbaalgos/ltl2tgba_fm.cc: Sort all maps to get deterministic results. Alexandre Duret-Lutz 2005-01-20 17:33:55 +00:00
8a5e31f00e * src/tgbaalgos/tau03opt.hh (explicit_tau03_opt_search): Doco. Alexandre Duret-Lutz 2005-01-18 16:10:49 +00:00
48dfd73cca * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo, couvreur99_check_shy::check): Sum all successors in the todo stack AND all items on the stack. Alexandre Duret-Lutz 2005-01-18 10:52:23 +00:00
2604b27008 * src/tgbaalgos/emptiness_stats.hh (ec_statistics::depth): New function. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo, couvreur99_check_shy::check): Count all successors in the todo stack rather than all items on the stack. Alexandre Duret-Lutz 2005-01-17 18:48:59 +00:00
addb3a30cd * src/tgbatest/randtgba.cc: Close the formula file and remove a trace. Denis Poitrenaud 2005-01-13 18:16:32 +00:00
2653b35ba7 * src/tgbatest/randtgba.cc: Add products with formulae issued of a file and more statistics. * src/tgbatest/readsave.test: Undo previous change. Denis Poitrenaud 2005-01-13 18:00:25 +00:00
4e6ce2e739 * src/tgbatest/readsave.test: Fix parameter of randtgba call. Denis Poitrenaud 2005-01-13 09:21:22 +00:00
333ee43f00 * src/tgbatest/randtgba.cc: Add products with randomized formulae and Denis Poitrenaud 2005-01-12 18:38:25 +00:00
0ff7f3ba2f * src/tgbaalgos/gv04.cc (result): Implement the acss_statistics, and ars_statistics interfaces. Alexandre Duret-Lutz 2005-01-11 14:42:00 +00:00
81423bb743 * src/ltltest/randltl.cc: Typo. Denis Poitrenaud 2005-01-11 12:37:43 +00:00
86b7f26960 * src/tgbaparse/tgbaparse.yy: Accept automaton without state. Denis Poitrenaud 2005-01-11 12:27:37 +00:00
3f2790061a * src/tgbatest/randtgba.cc: Typo. Denis Poitrenaud 2005-01-10 18:26:14 +00:00
1cc003ec38 * src/tgbatest/ltl2tgba.cc: Typo. Alexandre Duret-Lutz 2005-01-10 17:26:11 +00:00
6a0ab6c081 * src/tgbatest/randtgba.cc: Add option -P. Alexandre Duret-Lutz 2005-01-10 17:22:25 +00:00
a4b9b791ef * src/tgbaalgos/tau03.cc: Typo. * src/tgbatest/ltl2tgba.cc: Add option -b. Denis Poitrenaud 2005-01-10 17:17:19 +00:00
7c07f3149f * src/tgbaalgos/ndfs_result.hxx (ndfs_result, acss_interface): Conditionally inherit from acss_statistics. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Define Has_Size in all heaps. Alexandre Duret-Lutz 2005-01-07 10:27:17 +00:00
603b49e216 * src/ltltest/randltl.cc: Include cassert. Denis Poitrenaud 2005-01-06 15:54:48 +00:00
174b531f82 * src/ltltest/randltl.cc: Add options -r and -u. * src/ltltest/reduc.test: Use randltl -u, and run it through valgrind. Alexandre Duret-Lutz 2005-01-06 12:29:56 +00:00
e366b081a8 * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): Distribute them. * src/ltltest/randltl.cc: New file. * src/ltltest/Makefile.am (LDADD): Link with ../libspot.la directly. (noinst_PROGRAMS, randltl_SOURCES): New. (EXTRA_DIST, CLEANFILES): The list of random formulae is now generated. * src/ltltest/formulae.txt: Delete. * src/ltltest/reduc.test: Use randltl to generate formulae. * src/ltlvisit/length.cc (length_visitor): Fix computation of the length of multops. * src/ltlvisit/length.hh (length): Document the length of multops. Alexandre Duret-Lutz 2005-01-05 16:20:21 +00:00
7216701631 * src/sanity/includes.test: Also check *.hxx files. * src/tgbaalgos/ndfs_result.hxx: Rename the include guard. Alexandre Duret-Lutz 2005-01-04 13:32:53 +00:00
e9beca0d56 fix eof, truncated by last commit Alexandre Duret-Lutz 2005-01-04 13:20:50 +00:00
b054139e6d * doc/Doxyfile.in (FILE_PATTERNS): Remove *.hxx. * src/sanity/80columns.test, src/sanity/style.test: Process *.hxx files. * src/tgbaalgos/ndfs_result.hh: Rename as .. * src/tgbaalgos/ndfs_result.hxx: ... this, so it does not get documented (and so Doxygen do not complain). * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust include. * src/tgbaalgos/Makefile.am: Rename ndfs_result.hh as ndfs_result.hxx and do not install it, this is a private header. Alexandre Duret-Lutz 2005-01-03 17:39:43 +00:00
a9ab303859 * src/tgbaalgos/emptiness.hh: Declare Doxygen group emptiness_check_stats. * src/tgbaalgos/emptiness_stats.hh: Use it. Alexandre Duret-Lutz 2005-01-03 16:59:53 +00:00
685c23a756 * doc/Doxyfile.in: Update for Doxygen 1.4.0, set DOT_MULTI_TARGETS, and disable GROUP_GRAPH (it causes segfault). * src/tgbaparse/public.hh (format_tgba_parse_errors): Complete Doxygen comment. Alexandre Duret-Lutz 2005-01-03 16:40:15 +00:00
55c08790fd * src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class. * 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. Alexandre Duret-Lutz 2005-01-03 15:49:50 +00:00
6feb92090d * src/tgbaalgos/bfssteps.hh (bfs_steps::finalize): Document. Alexandre Duret-Lutz 2005-01-03 14:20:08 +00:00
ca2fe6c711 * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. * 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. Alexandre Duret-Lutz 2005-01-03 13:10:35 +00:00
13183893dd * src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call erase() after splice(), splice() already removes the elements. Alexandre Duret-Lutz 2005-01-03 12:11:28 +00:00
000c041a95 * src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh, src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh, src/misc/bareword.hh, src/tgba/succiter.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbareduc.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/tau03opt.hh: Add or fix include guards. * src/sanity/includes.test: Check the presence of the include guard. Alexandre Duret-Lutz 2005-01-03 10:20:26 +00:00
93f77c5782 * src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc (index_and_insert): New function. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): Rewrite. (couvreur99_check_shy::clear_todo): New method. * src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::todo_item): New struct. * iface/gspn/ssp.cc (numbered_state_heap_ssp_semi::index_and_insert): New method. Alexandre Duret-Lutz 2004-12-29 15:29:26 +00:00
988dbbd367 * doc/Doxyfile.in (EXCLUDE_SYMLINKS): Set to YES, since we have no legitimate symlink in our source tree. Requested by Akim Demaille. Alexandre Duret-Lutz 2004-12-20 13:35:33 +00:00
8dbc9424c1 * src/tgbaalgos/ndfs_result.hh: Rewrite the computation of accepting runs. * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Add the method finalize witch compute (by default) the traversed path. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc: Fix a bug concerning the heap used for bit state hashing version and ajust the prototype of has_been_visited and pop_notify. * src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: ajust the prototype of has_been_visited and pop_notify. Denis Poitrenaud 2004-12-20 10:09:45 +00:00
0c2c12a80f * src/tgbaalgos/ndfs_result.hh: Include misc/hash.hh. Alexandre Duret-Lutz 2004-12-17 08:33:32 +00:00
e7a3ebb16a * src/tgbaalgos/reducerun.cc (reduce_run): Do not call erase() after splice(), splice() already remove the elements. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): Likewise. Alexandre Duret-Lutz 2004-12-16 23:13:33 +00:00
58aff37db9 * src/tgbatest/randtgba.cc: Add option -O, so we can profile each emptiness-check on its own. Alexandre Duret-Lutz 2004-12-16 21:49:46 +00:00
0efca0f644 * src/ltlparse/ltlscan.ll: Pass yyleng to the std::string constructor, 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. Alexandre Duret-Lutz 2004-12-16 12:33:37 +00:00
704f237a22 * src/tgbaparse/tgbaparse.yy: Cache parsed formulae to speedup reading of TGBAs with lots of identical conditions. Alexandre Duret-Lutz 2004-12-15 17:13:44 +00:00
752d4afc31 * src/tgba/bdddict.hh (bdd_dict) <fv_map, vf_map, ref_set, vr_map, free_annonymous_list_of_type>: Redeclare as std::map, instead of Sgi::hash_map. It proved to be faster. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict) <fv_map, vf_map>: Use the same definition as in bdd_dict. * tgbaalgos/reachiter.hh, tgbaalgos/replayrun.cc: Explicitly include misc/hash.hh. Alexandre Duret-Lutz 2004-12-15 16:23:07 +00:00
b0a51a0656 Adjust Swig rules for Swig 1.3.24 (and probably 1.3.23 too). Compiling the runtime in a separate modules is no longer required, and actually it does not work anymore... * wrap/python/swigpy.i: Remove. * wrap/python/Makefile.am (_swigpy.la): Remove all references. ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Do not use -noruntime. Alexandre Duret-Lutz 2004-12-15 12:59:46 +00:00
73c42db23d * src/tgbatest/ltl2tgba.cc: Add option -P. Alexandre Duret-Lutz 2004-12-14 18:40:57 +00:00
60f50d66e0 * src/tgbaalgos/ndfs_result.hh: Define the trace output stream. Denis Poitrenaud 2004-12-14 14:10:56 +00:00
964f856bb5 * src/tgbaalgos/ndfs_result.hh: New file factorizing the computation of accepting runs for ndfs emptiness check algoritms. * src/tgbaalgos/Makefile.am: Add it. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Remove the old result classes and use the new one. Denis Poitrenaud 2004-12-13 08:43:05 +00:00
abbd0eee07 * src/tgbaalgos/gtec/status.hh (couvreur99_check_status::cycle_seed): New attribute. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Fill cycle_seed. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Revamp to compute a cycle from the cycle_start, and then the shortest prefix to this cycle. Alexandre Duret-Lutz 2004-12-10 18:33:39 +00:00
27966c28f0 * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap::find): Clarify comment. Alexandre Duret-Lutz 2004-12-10 18:24:15 +00:00
3763c2c16b * src/tgba/tgbareduc.hh: Include tgbaalgos/gtec/nsheap.hh, not tgbaalgos/gtec/status.hh. Alexandre Duret-Lutz 2004-12-10 18:22:33 +00:00