alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • b5f4ba982c * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::dump_queue): Remove superfluous semicolon. Alexandre Duret-Lutz 2008-02-01 11:31:43 +00:00
  • fbbaef0ab8 * src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Add two assert(). This patch has been lying in my tree since 2007-04-30. Alexandre Duret-Lutz 2008-01-10 13:47:25 +00:00
  • cc0ca4ae54 This is something Soheib and I worked on back in July, but a intricate memory corruption bug prevented me to check the patch in. It took me two days to realize why find_state() must do a double loop over the candidates to check for equality before checking for inclusion(s). Alexandre Duret-Lutz 2008-01-08 13:42:39 +00:00
  • 8d1b5e40b0 Ahem... Pass the -R option to the right chmod. Alexandre Duret-Lutz 2007-12-08 17:01:47 +00:00
  • f797b37c32 chmod -R Alexandre Duret-Lutz 2007-12-08 09:54:23 +00:00
  • 06006a9dad fix Alexandre Duret-Lutz 2007-12-07 17:06:29 +00:00
  • c09c56fcd8 new file Alexandre Duret-Lutz 2007-12-07 14:02:58 +00:00
  • 87c700feb2 Keep libtool's files under CVS so that we don't use the broken Debian versions installed in build hosts during automatic builds. Alexandre Duret-Lutz 2007-11-29 11:27:12 +00:00
  • 34e7cb9c0d cleanup Alexandre Duret-Lutz 2007-11-23 09:52:33 +00:00
  • 16d27686d3 Dummy changelog to test commit hooks. Alexandre Duret-Lutz 2007-11-23 09:51:43 +00:00
  • 3d01dd2eef * m4/valgrind.m4: New file. * configure.ac: Use it. Alexandre Duret-Lutz 2007-11-22 15:28:34 +00:00
  • ec6bca7992 * wrap/python/cgi/ltl2tgba.in: Adjust to newer versions of swig. Alexandre Duret-Lutz 2007-10-05 13:06:38 +00:00
  • 089c315c28 * src/misc/bddalloc.cc (bdd_allocator::initialize): Disable the default GC handler. Reported by Kristin Yvonne Rozier <kyrozier@cs.rice.edu>. Alexandre Duret-Lutz 2007-09-19 19:52:49 +00:00
  • 894c864fd5 * src/kernel.c (bdd_default_gbchandler): Log garbage collection to stderr, not stdout. Reported by Kristin Yvonne Rozier <kyrozier@cs.rice.edu>. Alexandre Duret-Lutz 2007-09-19 18:58:20 +00:00
  • 44e4beca2e * src/tgbatest/ltl2tgba.cc (main): Correctly destroy unobservable events. Alexandre Duret-Lutz 2007-07-26 13:51:16 +00:00
  • b8fd421232 * iface/gspn/ltlgspn.cc: New option -L. * iface/gspn/ssp.cc, iface/gspn/ssp.hh (gspn_ssp_interface) support for a new option "pushfront". Alexandre Duret-Lutz 2007-07-23 13:56:34 +00:00
  • fd2033aaba * NEWS, configure.in: Bump version to 0.4a. Alexandre Duret-Lutz 2007-07-23 11:46:36 +00:00
  • 82583754cd * NEWS, configure.in: Bump version to 0.4. * HACKING, INSTALL, doc/Doxyfile.in, lbtt/INSTALL: Update to newer tools. Alexandre Duret-Lutz 2007-07-17 15:53:27 +00:00
  • 0dc53d3d2a * iface/gspn/ssp.cc (tgba_gspn_ssp_private_::~tgba_gspn_ssp_private_): Fix the declaration for GCC 4.1.2. * iface/gspn/gspn.cc (tgba_gspn_private_::~tgba_gspn_private_): Likewise. Alexandre Duret-Lutz 2007-07-16 14:28:54 +00:00
  • 3ffba1c988 * src/tgbatest/spotlbtt.test: Do not check -R1q -R1t -R2q -R2t. Alexandre Duret-Lutz 2007-06-21 12:50:07 +00:00
  • 034e0e44f1 typo Alexandre Duret-Lutz 2007-04-30 08:12:42 +00:00
  • eb6bde4dd4 * src/tgbatest/ltl2tgba.cc (main): Fix handing of -R1q -R1t -R2q -R2t. Add support for -r8/-fr8. Alexandre Duret-Lutz 2007-04-30 08:12:00 +00:00
  • 5d8727258d * src/ltlvisit/reduce.cc (reduce): Repeat the reduction as long as the formula changes, it makes more sense when combining algorithm. E.g. basic reductions can help language containment and vice-versa. Alexandre Duret-Lutz 2007-04-29 08:31:13 +00:00
  • f57097b991 * src/tgbatest/spotlbtt.test: Disable formula rewriting during construction. Alexandre Duret-Lutz 2007-04-20 12:29:51 +00:00
  • 78d37fa126 * src/ltltest/reduc.cc (main): More cases to test. * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit): Simplify the formula again after FX->XF and GX->XG permutations. This is so that formulae like GFXXa become GFa and not just GFXa. * src/ltlvisit/contain.cc (reduce_tau03_visitor): Fix a typo in the rules for i|j or i&j, resulting in missing simplifications. Alexandre Duret-Lutz 2007-04-19 16:45:51 +00:00
  • b1c820af4d * src/ltlvisit/contain.cc (reduce_tau03_visitor): Simplify the rules for "a U b" and "a R b", an implication check is enough. Alexandre Duret-Lutz 2007-04-19 12:10:22 +00:00
  • 21e2439d06 * src/misc/bddalloc.cc (bdd_allocator::initialize): Call bdd_isrunning() and don't run bdd_init() if it has already been called. Alexandre Duret-Lutz 2007-04-17 13:11:49 +00:00
  • 1eb47b1a94 * src/tgbaalgos/randomgraph.cc (random_graph): Fix the generation of the graph. Some states had no successors or duplicate transitions because of that bug. Alexandre Duret-Lutz 2007-02-06 17:31:14 +00:00
  • 3c7f1822df * HACKING: We need Bison 2.3. Alexandre Duret-Lutz 2006-08-30 12:13:28 +00:00
  • ac94af5791 * evtgbaparse/evtgbaparse.yy, ltlparse/ltlparse.yy, tgbaparse/tgbaparse.yy: Fix Bison warnings about unset $$. Alexandre Duret-Lutz 2006-08-30 12:11:28 +00:00
  • 94bf01a53c * src/tgbaparse/Makefile.am (tgbaparse_HEADERS): Also install location.hh and position.hh, since we no longer share those of ltlvisit. * src/evtgbaparse/Makefile.am (evtgbaparse_HEADERS): Likewise. Alexandre Duret-Lutz 2006-08-30 09:43:25 +00:00
  • 6cf223bba4 * src/ltlparse/public.hh: Work around Bison 2.3 unique guards. Alexandre Duret-Lutz 2006-08-17 09:32:49 +00:00
  • 641db2d77d * src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards. * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh: Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger flags, and call reduce_tau03. * src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the default. * src/ltlvisit/contain.cc: Style. * src/ltltest/reduc.cc: Simplify using the reduce() interface instead of reduce_tau03. * src/tgbatest/ltl2tgba.cc: Likewise. Add -fr5, -fr6, and -fr7 options. * src/tgbatest/spotlbtt.test: Remove cases using "-c", since its current implementation is not always correct (and apparently reduces less than -fr7). Alexandre Duret-Lutz 2006-08-16 15:41:00 +00:00
  • c055212326 * src/evtgbatest/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, src/evtgbaparse/parsedecl.hh, src/evtgbaparse/public.hh, src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh, src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy, src/tgbaparse/tgbascan.ll: Adjust for Bison 2.3. Use %name-prefix instead of the "#define yy ... " kludge. Alexandre Duret-Lutz 2006-08-01 16:35:06 +00:00
  • db98955e9d * src/ltlvisit/contain.hh, src/ltlvisit/contain.cc: Adjust to only check containment on demand. Alexandre Duret-Lutz 2006-07-24 09:28:01 +00:00
  • d4c9bf2b1e * src/ltlvisit/contain.hh, src/ltlvisit/contain.cc (reduce_tau03): New function, performing LTL reduction a la tauriainen.03.a83. * src/ltltest/equals.cc, src/ltltest/reduc.cc: Add support for the new reduction. * src/ltltest/reduc.test: Cut the test in half, and additionally test the new reduction. * src/ltltest/reduccmp.test: Run on the new reduction. * src/ltltest/Makefile.am: Adjust. * src/tgbatest/ltl2tgba.cc: Add new options to apply the reduction. * src/tgbatest/spotlbtt.test: Use them. Alexandre Duret-Lutz 2006-07-19 16:30:10 +00:00
  • 8cbec95253 * src/tgba/tgbaproduct.cc: Fix computation of common acceptance conditions. Alexandre Duret-Lutz 2006-07-19 16:07:54 +00:00
  • c412cd4cc3 * src/tgba/bdddict.cc, src/tgba/bdddict.cc (register_clone_acc): New function. * src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Use it to distinguish acceptance conditions that are identical in both operands. * src/tgbatest/explpro4.test: New file. * src/tgbatest/explpro2.test, src/tgbatest/Makefile.am: Adjust. Alexandre Duret-Lutz 2006-07-19 14:55:39 +00:00
  • cb9549e4d4 * src/tgbaalgos/ltl2tgba_fm.cc (language_containment_checker): Move ... * src/ltlvisit/contain.cc, src/ltlvisit/contain.hh (spot::ltl::language_containment_checker): ... in these new files. * src/ltlvisit/Makefile.am: Adjust. Alexandre Duret-Lutz 2006-07-19 07:27:51 +00:00
  • c2bc76816b * src/misc/memusage.cc, src/misc/memusage.hh: New files. * src/misc/Makefile.am: Add them. * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: Add a "vmsize" statistic. Alexandre Duret-Lutz 2006-07-18 09:29:42 +00:00
  • 9e97543e33 * src/tgba/bdddict.cc, src/tgba/bdddict.hh (free_annonymous_list_of): Rename as ... (free_anonymous_list_of): ... this, and correct their update on release. Also correct yesterday's the correction (ahem!). (dump): Improve verbosity. * src/misc/freelist.cc (free_list::remove, free_list::insert): Fix longstanding thinkos. (free_list::free_count): New function. Alexandre Duret-Lutz 2006-07-14 15:30:23 +00:00
  • 064319b3e4 Merge this fix from proviso-branch: 2006-05-22 Alexandre Duret-Lutz <adl@src.lip6.fr> * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Count the Alexandre Duret-Lutz 2006-07-14 14:17:18 +00:00
  • decd87dcbf * src/tgba/tgbabddconcrete.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, src/tgba/tgbatba.hh: Remove superfluous class qualifiers worrying gcc 4.1.2. Alexandre Duret-Lutz 2006-07-14 07:08:57 +00:00
  • 85c5c870db * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Add a new option "containment_checks" to enable some language containment checks (via emptiness checks) during the translation. This first attempt currently only use containment checks to merge states bisimulating each other. * src/tgbatest/ltl2tgba.cc: Bind this to option "-c". * src/tgbatest/spotlbtt.test: Check it. Alexandre Duret-Lutz 2006-07-13 18:42:55 +00:00
  • 49a78724a4 * src/tgba/bdddict.cc (bdd_dict::unregister_variable): Correctly call release_n(), not remove() to repopulated the freelist of anonymous BDD variables. New code I'm working on triggered an assertion inside remove(), but I'm surprised this bug hadn't manifested before ! Alexandre Duret-Lutz 2006-07-13 17:21:36 +00:00
  • e84647b30b * iface/gspn/common.hh, iface/gspn/common.cc, iface/gspn/gspn.cc, iface/gspn/ltlgspn.cc, iface/gspn/dottygspn.cc, iface/gspn/ssp.cc, iface/gspn/dottyssp.cc: s/exeption/exception/g. Alexandre Duret-Lutz 2006-06-13 15:42:26 +00:00
  • 983d12cc5a * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: (couvreur99_check_shy_ssp): Add a onepass_ attribute to disable the "shyness", and do not increment pos before calling find_state since gspn's implementation uses it. * iface/gspn/ssp.cc: Enable "onepass_" for all "shy" variants, and also fix find_state for the case where onepass_ is disabled (but I do not yet know why the latter fix isn't enough). Alexandre Duret-Lutz 2006-04-05 09:24:39 +00:00
  • 644b74f8c0 * src/tgbaalgos/gtec/gtec.cc: Add a third level hash, to split each container into lists of states with identical formula states. Alexandre Duret-Lutz 2006-02-15 16:10:11 +00:00
  • afd4ea0eb4 * iface/gspn/ltlgspn.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: New option (-e6) to disable inclusion check in the stack. Alexandre Duret-Lutz 2006-02-15 15:35:38 +00:00
  • bb47e31b1e * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh: Count the number of removed components. Alexandre Duret-Lutz 2006-02-15 13:41:37 +00:00
  • 857f0ac54e * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state, numbered_state_heap_ssp_semi): Implement a double hash_map using greatspn's new container() function. * iface/gspn/ssp.hh (gspn_ssp_interface): Add a doublehash option. * iface/gspn/ltlgspn.cc: Add option -1 to disable this optimization. Alexandre Duret-Lutz 2006-02-14 17:07:23 +00:00
  • ea9ee5d5c7 * src/tgbatest/ltl2tgba.cc: Pacify sanity.test. Alexandre Duret-Lutz 2006-02-11 08:26:04 +00:00
  • 5891679ce0 * src/tgbaparse/public.hh (tgba_parse): Take two environments instead of one : one for the atomic propositions, and one for the acceptance conditions. This way it's easy for the tools in iface/gspn/ to require some atomic proposition to be declared and allow any acceptance conditions (there is nothing to adjust in this files because of the default value of the argument). * src/tgbaparse/tgbaparse.yy: Adjust. * src/tgbatest/ltl2tgba.cc, src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc: Adjust calls. Alexandre Duret-Lutz 2006-02-10 16:41:17 +00:00
  • e5481ee3ac * src/tgbaparse/tgbaparse.yy (acc_decl): Diagnose acceptance conditions rejected by the environment. Alexandre Duret-Lutz 2006-02-10 16:16:46 +00:00
  • d2cf7199bc * iface/gspn/ltlgspn.cc (display_stats): New function. (main): Use it. * iface/gspn/ssp.cc: Add more counters for statistics. Alexandre Duret-Lutz 2006-02-10 14:38:35 +00:00
  • 723054ce80 * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state): Correctly update the emptiness statistics. Alexandre Duret-Lutz 2006-02-10 12:13:26 +00:00
  • ffd47e425e * iface/gspn/ssp.cc: Pacify sanity.test. Alexandre Duret-Lutz 2006-02-05 15:54:00 +00:00
  • a390fe0754 typos Alexandre Duret-Lutz 2006-02-03 10:31:48 +00:00
  • 2a843fab1a * iface/gspn/ssp.cc (spot): Typo. Alexandre Duret-Lutz 2006-02-03 09:45:13 +00:00
  • 236742aed8 * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): Reorganize this function so that syntactically there is only one loop over the successors, and not two. Call reintroduce the call to couvreur99_check_shy::state_index(), needed by SSP, and suppress that to index_and_insert introduced on 2004-12-29. Also split the "group" option in two: "group" and "group2". "group2" is the equivalent of the older "group", while the new "group" is weaker and faster. (couvreur99_check_shy::state_index): Change prototype as needed by the algorithm. * src/tgbaalgos/gtec/gtec.hh: Adjust. * src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc (index_and_insert): Remove. * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust to new prototype. * bench/emptchk/README, bench/emptchk/algorithms: Adjust references to group/group2. Alexandre Duret-Lutz 2006-02-02 13:46:04 +00:00
  • d9d4804bc9 * NEWS, configure.ac: Bump version to 0.3a. Alexandre Duret-Lutz 2006-01-30 08:40:33 +00:00
  • 05d0353d04 * NEWS, README, configure.ac: Update for version 0.3. Alexandre Duret-Lutz 2006-01-25 13:51:39 +00:00
  • 3751960ac8 * wrap/python/cgi/ltl2tgba.in: Fix degeneralisation and output of accepting runs. Alexandre Duret-Lutz 2006-01-24 14:45:03 +00:00
  • 851ca0d807 * wrap/python/spot.i: Wrap spot::emptiness_check_instantiator. * wrap/python/cgi/ltl2tgba.in: Offers all 6 emptiness check algorithms, and a text box for options. Alexandre Duret-Lutz 2006-01-10 09:00:59 +00:00
  • 396894f7a7 * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_cycle): Initialize tmp to suppress a GCC 4.0.1 warning (seen on Darwin). Alexandre Duret-Lutz 2006-01-05 20:01:18 +00:00
  • b47f4ab09b * src/tgbatest/defs.in (VALGRIND): Use --log-fd instead of --logfile-fd to please newer versions of Valgrind. * src/ltltest/defs.in, src/evtgbatest/defs.in: Likewise. Alexandre Duret-Lutz 2006-01-03 14:42:53 +00:00
  • 89aff72523 * src/ltlparse/ltlparse.yy (result): Do not assign to $$, it's useless. Suggested by Akim. Alexandre Duret-Lutz 2005-09-29 13:22:17 +00:00
  • f7fe379e60 * src/tgbatest/randtgba.cc: New option -H. * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics_copy): New class. Alexandre Duret-Lutz 2005-09-29 12:25:34 +00:00
  • d5fb32120f * src/tgbatest/randtgba.cc: New option -S. Alexandre Duret-Lutz 2005-09-27 11:42:03 +00:00
  • 8e00065d84 * src/tgbaalgos/lbtt.cc: Typo. Alexandre Duret-Lutz 2005-09-23 18:45:00 +00:00
  • b343e16b51 * src/tgbatest/randtgba.cc (default_algos): Test the "ordering" heuristic. Alexandre Duret-Lutz 2005-09-22 16:07:30 +00:00
  • 3f22bc17ff * src/tgbaalgos/tau03opt.cc: Include <vector>. (tau03_opt_search): Add option "ordering" (off by default). If enabled, initialize an explicit ordering for acceptance conditions into the new member "cond" (a vector of bdds). (project_acc): New helper function for projecting a set of acceptance conditions to a subset that maximizes the number of initial consecutive conditions covered by the set in the condition ordering. (dfs_blue): Implement the ordering heuristic. (dfs_red): Use a sentinel in condition_stack to avoid explicit checks for the stack's emptiness. Consider also the conditions in acc when checking for the completion of an accepting cycle. Fix the implementation of condition heuristic. Implement the ordering heuristic. Simplify the removal of elements from condition_stack (due to the way in which elements are pushed on the stack, there can be at most one element with a given depth in the stack at any one time). Alexandre Duret-Lutz 2005-09-22 15:28:10 +00:00
  • 5b6e79ad96 * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_prefix): Initialize tmp to suppress a GCC 4.0 warning. * src/ltltest/randltl.cc (main): Likewise with another variable. Alexandre Duret-Lutz 2005-09-06 13:15:15 +00:00
  • 048a5825de * src/ltlast/visitor.hh (visitor, const_visitor): Add empty virtual destructors. * src/tgba/tgbabddfactory.hh (tgba_bdd_factory): Likewise. * src/misc/hash.hh: Use the std namespace only with GCC 3.0, not with all compiler versions with minor version 0. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Fix friend declaration of ::spot::tgba_tba_proxy. Alexandre Duret-Lutz 2005-09-06 11:53:14 +00:00
  • 6bcc8c3ce1 * src/tgbaalgos/magic.hh: fixme is not a doxygen command. Use bug. Alexandre Duret-Lutz 2005-09-06 11:52:58 +00:00
  • 98fd480506 * README: Update lbtt references. Alexandre Duret-Lutz 2005-08-31 16:35:45 +00:00
  • cc4137e5ba * iface/gspn/ssp.cc: Typo in comment. Alexandre Duret-Lutz 2005-08-31 15:36:53 +00:00
  • 760945e678 update Alexandre Duret-Lutz 2005-08-31 15:36:42 +00:00
  • 9517cde264 Merge commit 'origin/lbtt-orig' into new-master Alexandre Duret-Lutz 2008-02-25 14:34:25 +01:00
  • 91df6cab77 fix status of lbtt's subtree. Apparently it was messed up during the cvsimport Alexandre Duret-Lutz 2008-02-23 00:17:42 +01:00
  • 17f76e371f * lbtt/: Merge lbtt 1.2.0. Alexandre Duret-Lutz 2005-08-31 15:30:38 +00:00
  • 0a12b942a4 Import of lbtt 1.2.0 Alexandre Duret-Lutz 2005-08-31 15:14:51 +00:00
  • 8a5fd909b3 * src/tgbaalgos/reductgba_sim_del.cc (parity_game_graph_delayed::get_relation): Disable for generalized automata, it's wrong. Alexandre Duret-Lutz 2005-06-06 13:53:56 +00:00
  • fc4f4f7288 * src/tgbaalgos/reductgba_sim_del.cc (parity_game_graph_delayed::nb_set_acc_cond): Simplify. Alexandre Duret-Lutz 2005-05-25 09:00:19 +00:00
  • 35aa277164 * sanity/style.test: Catch misuses of Sgi::. * tgba/tgbareduc.hh, tgbaalgos/reductgba_sim.cc, tgbaalgos/reductgba_sim.hh, tgbaalgos/reductgba_sim_del.cc: Fix them. Alexandre Duret-Lutz 2005-05-25 08:56:15 +00:00
  • 64d5de8fe1 * src/ltlvisit/syntimpl.cc: Fix a typo. Denis Poitrenaud 2005-05-16 15:19:13 +00:00
  • 5a39d40b2c * src/ltlvisit/syntimpl.cc: Fix detection of purely eventual formulae. Alexandre Duret-Lutz 2005-05-14 20:56:19 +00:00
  • 2e15a93525 * src/tgbaalgos/ltl2tgba_fm.cc: Fix handling of fair_loop_approx. Alexandre Duret-Lutz 2005-05-12 18:01:27 +00:00
  • 814ec7c2d0 * src/misc/hashfunc.hh (knuth32_hash): New function. * src/misc/hash.hh (ptr_hash): Use knuth32_hash. * src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory): Use ltl::formula_ptr_hash for acc_map_. Alexandre Duret-Lutz 2005-05-04 16:09:41 +00:00
  • 9063c5abb4 * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add the reduce_ltl argument. * src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4. * src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4. * bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled algorithms. Alexandre Duret-Lutz 2005-05-04 13:47:38 +00:00
  • 7ef117e3dc * bench/ltl2tgba/README: More instructions. * bench/Makefile.am (SUBDIRS): Add ltl2tgba. * README: Mention bench/ltl2tgba. Alexandre Duret-Lutz 2005-04-19 09:04:22 +00:00
  • a7cf769a24 * bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/formulae.ltl, bench/ltl2tgba/known, bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small: New files. * src/tgbatest/ltl2baw.pl: Move ... * bench/ltl2tgba/ltl2baw.in: ... here. * src/tgbatest/Makefile.am: Adjust. * configure.ac: Adjust. Alexandre Duret-Lutz 2005-04-15 13:38:23 +00:00
  • 7753938fe9 * src/tgbatest/ltl2tgba.cc (main): Delete the reduced automaton before the degeneralized automaton. Alexandre Duret-Lutz 2005-04-14 09:21:59 +00:00
  • 98236cf656 * doc/Makefile.am (doc, $(srcdir)/stamp): Ignore rm's errors. Alexandre Duret-Lutz 2005-04-13 16:28:10 +00:00
  • acf61d1a46 * README: Typos. Alexandre Duret-Lutz 2005-04-12 09:18:54 +00:00
  • 8721f65bdc * NEWS, configure.ac: Bump version to 0.2a. Alexandre Duret-Lutz 2005-04-08 22:44:26 +00:00
  • e00aadce5b * NEWS, configure.ac: Bump version to 0.2. Alexandre Duret-Lutz 2005-04-08 22:41:09 +00:00
  • 751424c9ec * bench/emptchk/README: Mention http://spot.lip6.fr/wiki/EmptinessCheckOptions for the syntax. Alexandre Duret-Lutz 2005-04-08 19:00:08 +00:00
  • 5d0f702383 * src/tgbaparse/tgbaparse.yy (acc_list): Do not explicitly delete an undeclared acceptance condition. * src/tgbaalgos/save.cc (print_acc): Unquote atomic propositions. Alexandre Duret-Lutz 2005-04-06 17:23:29 +00:00
  • d309c01941 * bench/emptchk/Makefile.am: Create reduced versions of the graphs. * bench/emptchk/pml2tgba.pl: Add option -r. * bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Also run on reduced graphs (this is fast). * bench/emptchk/README: Adjust. Alexandre Duret-Lutz 2005-04-06 16:31:32 +00:00