Commit graph

alarsyo/spot

Fork 0

0222c5e186 * src/misc/timer.cc, src/tgbatest/randtgba.cc: Format the statistics. Denis Poitrenaud 2004-12-10 18:15:20 +00:00
0fc279c56e * src/tgbatest/emptchkr.test: Tune the "big degeneralized" test so it actually explore some accepting automata. Alexandre Duret-Lutz 2004-12-10 16:23:05 +00:00
9782b822f0 * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::couvreur99_check_shy): Add the group option, and redefine todo as a list so it can be iterated over. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce couvreur99_shy- (for group=false) in addition to couvreur99_shy (for group=true). * iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi, couvreur99_check_ssp_shy): Use group=true; Alexandre Duret-Lutz 2004-12-10 16:16:38 +00:00
8b8257b157 * src/tgbaalgos/randomgraph.cc (random_graph): Do not use the pointer of the state created as keys in sets; otherwise the graph created depends on the memory layout. Alexandre Duret-Lutz 2004-12-10 15:10:19 +00:00
d4b9ebaaff * src/tgba/tgbaexplicit.cc (tgba_explicit::create_transition): Make sure to create the source state before the destination state. Alexandre Duret-Lutz 2004-12-09 08:20:12 +00:00
d645e0ac54 * src/tgbaalgos/emptiness.cc: Suppress a horrible space before a ')'. Denis Poitrenaud 2004-12-08 18:14:46 +00:00
446b85a842 * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (set_init_state): Return a pointer to the initial state. Denis Poitrenaud 2004-12-08 18:03:38 +00:00
8279667300 * src/tgbaalgos/replayrun.cc (replay_tgba_run): More comments. Alexandre Duret-Lutz 2004-12-08 15:44:17 +00:00
688587d700 * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh (tgba_explicit::create_transition(state*, const state*)): New function. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: (random_graph): Revamp the algorithm to call rand() less often. * src/tgbatest/randtgba.cc: Add option -0 to easy profiling. Alexandre Duret-Lutz 2004-12-08 15:39:15 +00:00
7917841fbe * src/misc/random.hh: Add include guard. Alexandre Duret-Lutz 2004-12-08 08:28:51 +00:00
541705a36a * src/misc/random.hh (nrand, bmrand, prand): New functions. (barand): New class. * src/misc/random.cc (nrand, bmrand, prand): New functions. * wrap/python/spot.i: Process src/misc/random.hh. Alexandre Duret-Lutz 2004-12-07 18:52:10 +00:00
d771a3a019 * src/misc/timer.cc: Do not include cassert, then. Alexandre Duret-Lutz 2004-12-07 18:05:19 +00:00
acfcade04a * src/tgbaalgos/tau03opt.cc: Fix a memory leak in the computation of accepting runs Denis Poitrenaud 2004-12-07 17:58:16 +00:00
e9b260c081 * src/misc/timer.cc: Include cassert. Alexandre Duret-Lutz 2004-12-06 09:04:59 +00:00
668666d246 * src/misc/timer.hh, src/misc/timer.cc: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/tgbatest/randtgba.cc: Use time_map to measure the algorithms. Add the -R option. * src/sanity/style.sh: Let me use `for (.*;;)'. Alexandre Duret-Lutz 2004-11-29 16:50:49 +00:00
0531dfe6e5 * src/tgbaalgos/tau03opt.cc: Add a first version of the computation of accepting runs Denis Poitrenaud 2004-11-29 10:36:21 +00:00
e58743dbb7 * src/tgbaalgos/minimizerun.cc, src/tgbaalgos/minimizerun.hh (minimize_run): Rename as ... * src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh: (reduce_run): ... this. * src/tgbaalgos/Makefile.am, src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Adjust all references. Alexandre Duret-Lutz 2004-11-29 10:01:08 +00:00
3c9f4c6d0d * src/tgbatest/emptchkr.test: Try degeneralized automata. * src/tgbatest/randtgba.cc (main): Pass the correct automaton to minimize_run(). Alexandre Duret-Lutz 2004-11-29 09:48:01 +00:00
13870bbaab * src/ltltest/equals.cc (main): Add option -E. * src/ltltest/parseerr.test: Use equals -E' instead of readltl' to check the parsing of erroneous strings without being sensible to the ordering for formulae in memory. Alexandre Duret-Lutz 2004-11-28 20:17:06 +00:00
896dc5afec * src/tgbatest/randtgba.cc (to_float): Use strtod() instead of strtof() to please Solaris 9. Alexandre Duret-Lutz 2004-11-28 19:42:10 +00:00
8b67d86e39 * configure.ac (AM_INIT_AUTOMAKE): Use option tar-ustar, we have filenames longer than 99 bytes. Alexandre Duret-Lutz 2004-11-28 18:08:08 +00:00
fdeea6dbf8 * wrap/python/tests/run.in: Do not override PYTHONPATH, just add to it. Report from Akim Demaille. Alexandre Duret-Lutz 2004-11-28 17:12:21 +00:00
c0ed084e7d * src/sanity/style.test: Make sure grep supports the options put into GREP_OPTIONS. Alexandre Duret-Lutz 2004-11-28 15:25:01 +00:00
b61fab1eb0 * wrap/python/tests/run.in: Define DYLD_LIBRARY_PATH so that Darwin finds non-installed libraries. Report from Akim Demaille. Alexandre Duret-Lutz 2004-11-28 13:52:27 +00:00
39ffa27338 * src/tgbatest/ltl2tgba.cc (syntax): Mention gv04 in help text. Alexandre Duret-Lutz 2004-11-28 12:48:51 +00:00
a5608a7ec4 * src/tgbaalgos/minimizerun.cc: Shut up a GCC warning when assert are disabled. Alexandre Duret-Lutz 2004-11-27 01:03:43 +00:00
6724f4bfbb * src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them/ * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m. * src/tgbatest/emptchkr.test: Use -m. Alexandre Duret-Lutz 2004-11-26 23:54:53 +00:00
15329c5618 * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix comments and debug traces Denis Poitrenaud 2004-11-25 14:40:17 +00:00
2143d6c4b6 * src/tgbatest/randtgba.cc: Add option -D. Alexandre Duret-Lutz 2004-11-25 12:52:01 +00:00
f47f955a34 * src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result): Add the TGBA considered as a protected attribute, and provide an automaton() accessor. * src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow this new interface. Alexandre Duret-Lutz 2004-11-25 12:51:04 +00:00
16e54b2fc4 * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Revert previous change (bfs_steps_with_path_conditions turned up useless), and document bfs_step. Alexandre Duret-Lutz 2004-11-24 17:47:48 +00:00
18b22a5250 * src/tgbaalgos/bfssteps.hh (bfs_steps_with_path_conditions): New class. * src/tgbaalgos/bfssteps.cc: Remove includes that are now superfluous. Alexandre Duret-Lutz 2004-11-24 16:31:21 +00:00
c1fd4d1138 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Rewrite the BFSs using the bfs_steps class. Alexandre Duret-Lutz 2004-11-24 15:36:56 +00:00
2b74398a62 * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/gv04.cc (gv04::result::accepting_run): Use the new bfs_steps class. Alexandre Duret-Lutz 2004-11-24 14:38:21 +00:00
df1bf80d1f * src/tgbaalgos/gv04.cc (gv04::result): New struct to compute counter examples. (gv04:check): Return a gv04::result. Alexandre Duret-Lutz 2004-11-23 18:39:12 +00:00
976a86ba2b * src/tgbaalgos/tau03opt.cc: Fix a warning. Denis Poitrenaud 2004-11-23 13:54:34 +00:00
b0aab51580 * src/tgbaalgos/gv04.cc (gv04): Inherit from ec_statistics. (gv04::check, gv04::push, gv04::pop): Update the statistics for randtgba. (gv04::print_stats): Print them here too. Alexandre Duret-Lutz 2004-11-22 17:50:43 +00:00
f965894a7f * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Compute more statistics for randtgba. (couvreur99_check::print_stats): Print these here too. Alexandre Duret-Lutz 2004-11-22 17:41:38 +00:00
63453a2424 * src/sanity/style.test: Allow "'" after ",". Alexandre Duret-Lutz 2004-11-22 17:06:25 +00:00
6cce60bed7 * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and src/tgbaalgos/tarjan_on_fly.hh former implementation. * src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES, tgbaalgos_HEADERS): Add them. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the new algorithm. * src/tgbatest/emptchk.test: Test it. Alexandre Duret-Lutz 2004-11-22 16:57:31 +00:00
0f15d28fe8 * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, src/tgbaalgos/weight.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics capability. * src/tgbatest/randtgba.cc: Print these statistics. * src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance condition. * src/tgbatest/emptchk.test: Test tau03opt search. Denis Poitrenaud 2004-11-22 12:06:03 +00:00
fc775a8b1f * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: Fix copyright year, and do not include <iterator>. Alexandre Duret-Lutz 2004-11-19 13:29:39 +00:00
8068a54e38 * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. (ce_stat): New struct. Alexandre Duret-Lutz 2004-11-18 19:05:41 +00:00
121d582480 * src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo. * src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now the original one. * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files implementing most of all the optimisations of tau03. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public. * src/tgbatest/tba_samples_from_spin.test: Test them. Denis Poitrenaud 2004-11-18 16:09:41 +00:00
321177331d * src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/stats.hh: Typos. Alexandre Duret-Lutz 2004-11-17 17:45:01 +00:00
a1262a30fb * src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files from tba_samples_from_spin. * src/tgbatest/tba_samples_from_spin.test: Get these example files from $srcdir, for the sake of VPATH builds. (light_run): Remove, not needed. Alexandre Duret-Lutz 2004-11-17 17:42:19 +00:00
2a3d638a50 * src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh, src/misc/escape.hh, src/misc/freelist.hh, src/misc/hash.hh, src/misc/hashfunc.hh, src/misc/minato.hh, src/misc/modgray.hh, src/misc/random.hh, src/misc/version.hh, src/tgba/state.hh: More Doxygen groups. Alexandre Duret-Lutz 2004-11-17 17:20:44 +00:00
9bea364e40 * src/tgbaalgos/magic.hh: Fix a comment and remove se05 interface. * src/tgbaalgos/magic.cc: Fix a comment. * src/tgbaalgos/se05.hh: New file. * src/tgbaalgos/se05.cc: Fix a comment. * src/tgbaalgos/tau03.hh: New file. * src/tgbaalgos/tau03.cc: New file. * src/tgbaalgos/Makefile.am: Add it. * src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check. * src/tgbatest/randtgba.cc: Add tau03 new emptiness check. * src/tgbatest/emptchkr: Fix a comment. * src/tgbatest/tba_samples_from_spin/explicit1_1.tba, src/tgbatest/tba_samples_from_spin/explicit1_2.tba, src/tgbatest/tba_samples_from_spin/explicit1_3.tba, src/tgbatest/tba_samples_from_spin/explicit1_4.tba, src/tgbatest/tba_samples_from_spin/explicit1_5.tba, src/tgbatest/tba_samples_from_spin/explicit1_6.tba, src/tgbatest/tba_samples_from_spin/explicit1_7.tba, src/tgbatest/tba_samples_from_spin/explicit1_8.tba, src/tgbatest/tba_samples_from_spin/explicit1_9.tba, src/tgbatest/tba_samples_from_spin/explicit2_1.tba, src/tgbatest/tba_samples_from_spin/explicit2_2.tba, src/tgbatest/tba_samples_from_spin/explicit2_3.tba, src/tgbatest/tba_samples_from_spin/explicit2_4.tba, src/tgbatest/tba_samples_from_spin/explicit2_5.tba, src/tgbatest/tba_samples_from_spin/explicit2_6.tba, src/tgbatest/tba_samples_from_spin/explicit2_7.tba, src/tgbatest/tba_samples_from_spin/explicit2_8.tba, src/tgbatest/tba_samples_from_spin/explicit2_9.tba: New files * src/tgbatest/tba_samples_from_spin.test : New test. * src/tgbatest/Makefile.am: Add it. Denis Poitrenaud 2004-11-17 17:07:25 +00:00
c3e399c837 * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh, src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms. Alexandre Duret-Lutz 2004-11-17 16:56:36 +00:00
36aadba740 * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh, src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh, src/ltlparse/public.hh, src/ltlvisit/apcollect.hh, src/ltlvisit/basicreduce.hh, src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh: Add Doxygen groups for LTL algorithms and types. * doc/Makefile.am (fast-doc): New target. Alexandre Duret-Lutz 2004-11-17 16:23:40 +00:00
8c6dff00b6 * src/misc/hashfunc.hh: Include cstddef to define size_t, and guard the file for multiple inclusions. Alexandre Duret-Lutz 2004-11-17 00:56:26 +00:00
2cd298e4b0 * src/tgba/bdddict.hh, src/tgba/state.hh, src/tgba/statebdd.hh, src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, src/tgba/tgbatba.hh, src/tgbaalgos/emptiness.hh, src/tgbaalgos/magic.hh, src/tgbaalgos/replayrun.hh, src/tgbaalgos/gtec/gtec.hh, iface/gspn/ssp.hh: Introduce Doxygen groups in the documentation. Presently this only covers the tgba/ directory, and the emptiness-check algorithms. * doc/Doxyfile.in (EXCLUDE_PATTERNS): Skip Bison-generated files in src/evtgbaparse/. Alexandre Duret-Lutz 2004-11-16 23:47:50 +00:00
cac85dbcca * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the functionality of the old tgba_tba_proxy. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator, tgba_tba_proxy): Rewrite to produce TBA with at most N copies of each state, skipping the `bddtrue' stage now used only in tgba_sba_proxy. Doing so removes approximately 6% of states in the degeneralized tests of spotlbtt.test. (tgba_sba_proxy): Implement it. * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust to take a tgba_sba_proxy. * src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to never_claim_reachable(). Alexandre Duret-Lutz 2004-11-16 18:38:19 +00:00
ee5462105b * src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash. * src/tgba/tgbaproduct.cc (state_product::hash): Likewise. Alexandre Duret-Lutz 2004-11-16 15:38:22 +00:00
dfb832cf20 * src/misc/hashfunc.hh (wang32_hash): New file and function, extracted from... * src/evtgba/product.cc (evtgba_product_state::hash): ... here. * src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh. Alexandre Duret-Lutz 2004-11-16 14:59:49 +00:00
49b871f924 * src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness check, degeneralize the automaton only if it has too much acceptance conditions. This makes it easier to reproduce runs of randtgba. * src/tgbatest/emptchk.test: Adjust. Alexandre Duret-Lutz 2004-11-16 00:35:18 +00:00
dd4d8dea01 * src/tgbaalgos/magic.cc: Fix a stupid bug. * src/tgbaalgos/se05.cc: Fix the same bug. * src/tgbatest/Makefile.am: Signify that emptchkr.test pass. Denis Poitrenaud 2004-11-15 18:15:42 +00:00
5d16bb63b4 * tgbatest/randtgba.cc: Add options -e and -r. * tgbatest/emptchkr.test: New file. * src/tgbatest/Makefile.am (TESTS, XFAIL_TESTS): Add emptchkr.test. Alexandre Duret-Lutz 2004-11-15 16:51:12 +00:00
ea9af1f1b0 * src/tgbaalgos/replayrun.cc (replay_tgba_run): Fix a memory leak if debug==false. Alexandre Duret-Lutz 2004-11-15 15:07:21 +00:00
78be35142d * src/tgbaalgos/randomgraph.cc (random_graph): Do declare all the acceptance conditions in the produced automaton, in case they are not actually used. Alexandre Duret-Lutz 2004-11-15 13:29:04 +00:00
d6f865ac13 * src/tgbaalgos/replayrun.cc (replay_tgba_run): Write to the supplied stream, not std::cout. Alexandre Duret-Lutz 2004-11-15 13:27:55 +00:00
3ea9771942 * src/tgbaalgos/magic.cc: Add a bit state hashing version. * src/tgbaalgos/se05.cc: Add a bit state hashing version. * src/tgbaalgos/magic.hh: Make them public. * src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks. * src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test. * src/tgbatest/dfs.test: Introduce new characteristic explicit tests. Denis Poitrenaud 2004-11-15 12:16:59 +00:00
ca6084160e * wrap/python/cgi/ltl2tgba.in: Add options to check the produced automata for emptiness, using the existing algorithms. * wrap/python/spot.i: Declare spot::explicit_magic_search, and spot::explicit_se05_search as allocating their output. Alexandre Duret-Lutz 2004-11-14 23:10:56 +00:00
4a7486bbff * configure.ac: Check for srand48 and drand48. * src/misc/random.cc (srand, drand): Use srand48 and drand48 if available. Alexandre Duret-Lutz 2004-11-12 18:27:09 +00:00
5bcb6091fd * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS) (libtgbaalgos_la_SOURCES): Add them. * src/tgba/tgbaexplicit.hh (tgba_explicit::add_state): Make it public. * src/tgbatest/randtgba.cc: New file. * src/tgbatest/Makefile.am (noinst_PROGRAMS, readsave_SOURCES): Add it. * src/tgbatest/readsave.test: Check a random graph. Alexandre Duret-Lutz 2004-11-12 17:24:46 +00:00
e54ddd46ed * misc/random.cc, misc/random.hh: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. Alexandre Duret-Lutz 2004-11-12 16:27:39 +00:00
67e133ae51 * src/evtgbaparse/public.hh (evtgba_parse): Fix doxygen comments. * src/tgbaalgos/projrun.hh (project_tgba_run): Likewise. Alexandre Duret-Lutz 2004-11-10 14:14:05 +00:00
57792ca541 * src/tgbaalgos/emptiness.hh (print_tgba_run): Document it. Alexandre Duret-Lutz 2004-11-10 14:09:37 +00:00
21e0e9bc18 * src/tgbaalgos/replayrun.hh, src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug' option to decide whether the output should look like that of print_tgba_run() or a complete debug trace. * src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with debug=true. Alexandre Duret-Lutz 2004-11-10 13:56:42 +00:00
a67e2d0b23 * iface/gspn/ltlgspn.cc (main): Adjust to recent changes to src/tgbaalgos/magic.cc, call explicit_magic_search() instead of building a spot::magic_search. * iface/gspn/udcseltl.test: Adjust to new output of print_tgba_run(). Alexandre Duret-Lutz 2004-11-10 12:28:47 +00:00
9b4edbc387 * src/tgbatest/Makefile.am (TESTS): Remove non-existing magic.test and se05.test. Alexandre Duret-Lutz 2004-11-09 18:13:27 +00:00
dc634800bf * src/tgbatest/ltl2tgba.cc (syntax): Fix old typos and reword some help strings. Alexandre Duret-Lutz 2004-11-09 18:08:42 +00:00
f52082bcfb * src/tgbaalgos/magic.cc: rewrite to externalize the heap and prepare it to a bit state hashing version. * src/tgbaalgos/magic.hh: adapt to the new interface of magic_search and se05_search. * src/tgbaalgos/se05.cc: new file. * src/tgbaalgos/Makefile.am: Add it. * src/tgbatest/ltl2tgba.cc: Add new emptiness check. * src/tgbatest/emptchk.test: more tests. * src/tgbatest/dfs.test: new file. * src/tgbatest/Makefile.am: Add it. Denis Poitrenaud 2004-11-09 17:22:58 +00:00
908b6129f4 * src/tgbaalgos/emptiness.cc (print_tgba_run): Output the labels as formulae rather than bdd sets. Alexandre Duret-Lutz 2004-11-09 10:41:25 +00:00
9d0bcae806 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path): Rewrite as ... (couvreur99_check_result::accepting_cycle): ... this less complex implementation. (couvreur99_check_result::complete_cycle): Delete. * src/tgbatest/emptchke.test: More explicit examples. Alexandre Duret-Lutz 2004-11-08 17:39:48 +00:00
263afcd22a * src/tgbaalgos/replayrun.cc (replay_tgba_run): Do not leak the initial state when no valid outgoing transition is found. Alexandre Duret-Lutz 2004-11-08 15:39:52 +00:00
7afd10420a * src/tgbaparse/tgbaparse.yy: Add `%destructor's so the parser does not leak on errors. * src/tgbatest/ltl2tgba.cc: Free the automata if it could not be fully parsed. Alexandre Duret-Lutz 2004-11-08 14:43:10 +00:00
86ff462fa4 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): Remove spurious FIXME. Alexandre Duret-Lutz 2004-11-08 10:32:34 +00:00
a31ab32b9b * src/evtgbaalgos/save.cc (save_bfs::output_acc_set): Sort acceptance conditions in the output. * src/evtgbatest/readsave.test, src/evtgbatest/product.test: Adjust. Alexandre Duret-Lutz 2004-11-05 17:26:33 +00:00
6c1152d819 * src/tgbaalgos/rundotdec.cc (tgba_run_dotty_decorator::link_decl): Typo. Alexandre Duret-Lutz 2004-11-05 06:46:47 +00:00
9444d84a17 * src/tgbaalgos/neverclaim.cc (never_claim_bfs::process_link): Adjust prototype. Alexandre Duret-Lutz 2004-11-04 12:57:04 +00:00
d60025dcd1 * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::number_of_acceptance_conditions): New method. * src/tgbaalgos/lbtt.cc (lbtt_bfs::lbtt_bfs): Use it. Alexandre Duret-Lutz 2004-11-04 12:55:03 +00:00
1d3100607a * wrap/python/spot.i: Generate bindings for tgbaalgos/dottydec.hh, tgbaalgos/emptiness.hh, tgbaalgos/gtec/gtec.hh, and tgbaalgos/rundotdec.hh. Alexandre Duret-Lutz 2004-11-04 08:03:59 +00:00
c3d50ed019 * src/tgbaalgos/lbtt.cc (lbtt_bfs::process_link): Adjust prototype. Alexandre Duret-Lutz 2004-11-04 06:59:47 +00:00
7688431451 * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh, src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator as third parameter. * src/tgbaalgos/dotty.cc (dotty_bfs::process_state, dotty_bfs::process_link): Use the decorator. * src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option is given. * src/tgbatest/emptchk.test: Exercize -g. Alexandre Duret-Lutz 2004-11-03 15:17:06 +00:00
a90b0648f8 * src/tgbaalgos/replayrun.cc (replay_tgba_run): Add missing std::endl. Alexandre Duret-Lutz 2004-11-03 12:35:37 +00:00
42b05c7a05 * tgbaalgos/reachiter.hh, tgbaalgos/reachiter.cc (tgba_reachable_iterator::process_link): Take the state* as arguments in addition to the state numbers. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (tgba_explicit::copy_acceptance_conditions_of): New method. * tgbaalgos/dupexp.cc (dupexp_iter::dupexp_iter): Call copy_acceptance_conditions_of. (dupexp_iter::process_state, duplex_iter::declare_state, dupexp_iter::name_): Remove. (dupexp_iter::process_link): Adjust prototype, and format the state here rather than in process_state. * tgbaalgos/stats.cc, tgbaalgos/dotty.cc: Adjust prototype of process_link. Alexandre Duret-Lutz 2004-11-03 11:59:58 +00:00
b6f3faba38 * src/ltlvisit/reduce.hh (is_eventual, is_universal): More doc. Alexandre Duret-Lutz 2004-11-02 17:16:32 +00:00
e3de75f677 * src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * iface/gspn/ltlgspn.cc (main): Call project_tgba_run if -P. Alexandre Duret-Lutz 2004-11-02 16:26:57 +00:00
0fd665f3a2 * src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba* argument before the tgba_run* argument (for consistency with replay_tgba_run). * src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust calls to print_tgba_run(). Alexandre Duret-Lutz 2004-11-02 15:25:41 +00:00
e5e886a442 * src/ltlast/formula.hh (ltl::formula::~formula): Make it protected. Alexandre Duret-Lutz 2004-11-02 13:53:20 +00:00
754d7064ae A tgba can now annotate a transition (i.e., the position of a tgba_succ_iterator) with some string. This comes handy to associate that transition to its high-level name. * src/tgba/tgba.hh, src/tgba/tgba.cc (tgba::transition_annotation): New method. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (tgba_product::transition_annotation): Implement it. * src/tgba/tgbatba.hh, src/tgba/tgbatba.cc (tgba_tba_proxy::transition_annotation): Likewise. * src/tgbaalgos/replayrun.cc (print_annotation): New function. (replay_tgba_run): Use it. Alexandre Duret-Lutz 2004-10-29 16:45:49 +00:00
32403566f6 * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New. * src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics. Alexandre Duret-Lutz 2004-10-29 16:10:47 +00:00
55014e9dcc * src/sanity/style.test: Diagnose superfluous constructs such as `if (x) delete x;'. * iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/magic.cc, src/tgbatest/ltl2tgba.cc: Remove such constructs. Alexandre Duret-Lutz 2004-10-29 14:29:02 +00:00
4654da9ab5 * src/tgbatest/ltl2tgba.cc: Replace -e, -E, -m, -M, and -n by -eALGO and -EALGO to ease the addition of new algorithms. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust. Alexandre Duret-Lutz 2004-10-29 13:15:01 +00:00
7fce2b2a95 * src/misc/version.cc: Fix trailing whitespace. * src/sanity/style.test: Diagnose trailing whitespace. Alexandre Duret-Lutz 2004-10-29 12:41:56 +00:00
8c0b085d73 * src/tgbatest/ltl2tgba.cc: Fix lines longer than 80 chars. * src/sanity/80columns.test: Use expand to untabify, the previous recipe was incomplete. Alexandre Duret-Lutz 2004-10-29 12:31:13 +00:00
720a31c128 * src/tgbaalgos/replayrun.cc (replay_tgba_run): Note duplicate states. Alexandre Duret-Lutz 2004-10-29 12:19:18 +00:00
cf45539312 * src/tgbaalgos/replayrun.cc (replay_tgba_run): Verify the run is accepting. Alexandre Duret-Lutz 2004-10-29 11:51:21 +00:00
434475dbc8 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_path): Initialize best_end to remove a spurious warning. Alexandre Duret-Lutz 2004-10-29 07:05:30 +00:00