Commit graph

Select branches

Hide pull requests

am/merged-work

am/nix

am/psl-derivation

am/psl2aa

am/sonf

am/thesis-fixes

Mono Color

• 98604c754f * src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ... * src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match the function name. * ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am, tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames. Alexandre Duret-Lutz 2004-06-22 22:54:35 +00:00
• 473af5bb1d * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)): Factorize. Alexandre Duret-Lutz 2004-06-22 22:48:34 +00:00
• 47e9ac108f * src/ltlvisit/basicreduce.hh: New file, extracted from ... * src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/basereduc.cc: Rename as ... * src/ltlvisit/basicreduce.cc: ... this, to match the function name. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES): Adjust filenames. * src/ltlvisit/reducform.cc: Adjust includes. Alexandre Duret-Lutz 2004-06-22 22:27:53 +00:00
• a57c619ed5 * src/ltlvisit/lunabbrev.hh: Revert superfluous change from 2004-05-10. Alexandre Duret-Lutz 2004-06-22 22:06:28 +00:00
• 2f1a67d927 * src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc: 80 columns and style. martinez 2004-06-22 17:24:46 +00:00
• f61b69ef3d * src/sanity/style.test: Typo. Alexandre Duret-Lutz 2004-06-22 17:12:14 +00:00
• eb0852257f * src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc: bug in delayed simulation. martinez 2004-06-22 15:30:12 +00:00
• 6d5593ae48 * src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc: There is bug in reduction with scc. * src/tgbatest/reduccmp.test: More test. martinez 2004-06-21 12:15:19 +00:00
• f680eb0d80 * src/tgbatest/reductgba.test, src/ltltest/reduccmp.test: Wrong test are removed. martinez 2004-06-17 17:00:29 +00:00
• cc93a6d6ac * src/ltltest/reduccmp.test: Wrong test are removed. martinez 2004-06-17 16:48:22 +00:00
• c769f74750 * src/tgbatest/spotlbtt.test: We don't check the post-reduction with scc and delayed simulation. martinez 2004-06-17 16:27:36 +00:00
• 84e72c8764 * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s. This fixes a memory leak observed by Soheib Baarir. Alexandre Duret-Lutz 2004-06-17 09:07:36 +00:00
• 525c8918ca * src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test: Test for reduction of tgba. martinez 2004-06-16 09:31:43 +00:00
• 8d3606ff07 * src/tgbatest/ltl2tgba.cc: Add some option for the reduction of automata. * src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some test for reduction of automata. * src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation to reduce a tgba. * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation of tgba for the reduction. * src/tgbaalgos/Makefile.am, src/tgba/Makefile.am: Add the reduction of automata. * src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc: Lot of mistake are corrected. * src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust. * src/ltltest/equals.cc, src/ltltest/reduccmp.test, src/ltltest/Makefile.am: Add a test for reduction. martinez 2004-06-15 16:24:02 +00:00
• 383f7e170a * iface/gspn/common.cc, iface/gspn/common.hh: Remove the class gspn_environment, and move it to ... * src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file as class declarative_environment. * src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh. (libltlenv_la_SOURCES): Add declenv.cc. * iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc, iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc, iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references to declarative_environment. Alexandre Duret-Lutz 2004-06-02 16:21:49 +00:00
• 8e324fa2a2 * HACKING, src/sanity/style.test: NULL is not portable, prohibit it. * iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc, src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/syntimpl.cc: Use 0 instead of NULL. Alexandre Duret-Lutz 2004-06-02 15:16:47 +00:00
• 6e3fd873ba * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ... * src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these. * src/ltltest/Makefile.am: Adjust. * src/ltlvisit/forminf.cc: Rename as... * src/ltlvisit/syntimpl.cc: ... this. * src/ltlvisit/syntimpl.hh: New file with definitions extracted from ... * src/ltlvisit/reducform.hh: ... this one. * src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust. Alexandre Duret-Lutz 2004-06-01 20:43:00 +00:00
• 121a55c48f * src/ltlvisit/forminf.cc (form_eventual_universal_visitor, inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename as ... (eventual_universal_visitor, inf_right_recurse_visitor, inf_left_recurse_visitor): ... these. (is_GF, is_FG): Move ... * src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they are only used here. (basic_reduce_form, basic_reduce_form_visitor): Rename as ... (basic_reduce, basic_reduce_visitor): ... these. * src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ... (reduce_visitor): ... this. * src/ltltest/inf.cc: Adjust calls. * src/sanity/style.test: Improve missing-space after coma detection. Alexandre Duret-Lutz 2004-05-30 12:33:35 +00:00
• c0b59d0795 * src/ltlvisit/reducform.cc (reduce_form_visitor::visit(constant)): Simplify. Alexandre Duret-Lutz 2004-05-26 16:54:02 +00:00
• cdbb199c4d * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc: Use dynamic_cast instead of node_type_form_visitor, this is usually smaller. * src/ltlvisit/reducform.hh, src/ltlvisit/forminf.cc (node_type_form_visitor): Delete. * src/sanity/style.test: Two more checks. Alexandre Duret-Lutz 2004-05-26 12:48:22 +00:00
• d973c1dad0 * src/ltlvisit/formlength.cc: Rename as ... * src/ltlvisit/length.cc: ... this. * src/ltlvisit/length.hh: New file, extracted from ... * src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh. (libltlvisit_la_SOURCES): Rename formlength.cc as length.cc. * src/ltltest/reduc.cc: Include length.hh. Alexandre Duret-Lutz 2004-05-25 23:08:19 +00:00
• f17af7a761 * src/ltlvisit/formlength.cc: Rename as ... * src/ltlvisit/length.cc: ... this. * src/ltlvisit/length.hh: New file, extracted from ... * src/ltlvisit/reducform.hh: ... here. * src/ltlvisit/Makefile.am (ltlvisit_HEADERS): Add length.hh. (libltlvisit_la_SOURCES): Rename formlength.cc as length.cc. * src/ltltest/reduc.cc: Include length.hh. Alexandre Duret-Lutz 2004-05-25 13:20:30 +00:00
• e0ec45ed14 * src/ltlvisit/formlength.cc (length_form_vistor): Rename as .. (length_visitor): ... this. (form_length): Rename as ... (length): ... this. * src/ltlvisit/reducform.hh (form_length): Rename as ... (length): ... this. * src/ltltest/reduc.cc: Adjust. Alexandre Duret-Lutz 2004-05-25 13:08:33 +00:00
• 92767ce9d2 * src/ltlvisit/basereduc.cc, src/ltlvisit/formlength.cc: Remove useless includes. Alexandre Duret-Lutz 2004-05-25 13:02:36 +00:00
• 52a672ec7e * AUTHORS: Update. Alexandre Duret-Lutz 2004-05-25 12:58:13 +00:00
• 20bdf49a70 * src/ltlvisit/reducform.hh: Update Doxygen comments for previous change. Alexandre Duret-Lutz 2004-05-25 12:55:48 +00:00
• 8f82f1d5f3 * src/ltlvisit/reducform.hh (option): Rename as ... (reduce_options): ... this, and use it as a bit field so option can be combined easily. (reduce): Adjust argument. (reduce_form): Remove, not needed anymore. * src/ltlvisit/reducform.cc, src/ltltest/reduc.cc, src/tgbatest/ltl2tgba.cc: Adjust. Alexandre Duret-Lutz 2004-05-25 12:46:56 +00:00
• 7eb5f3d81a * src/sanity/style.test: Catch {.*{ and }.*}. * src/sanity/80columns.test: Untabify files. * iface/gspn/ltlgspn.cc, src/ltlvisit/basereduc.cc: Fix long lines. Alexandre Duret-Lutz 2004-05-25 11:05:07 +00:00
• 3426ece95c * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes. Alexandre Duret-Lutz 2004-05-25 09:14:51 +00:00
• c68d182951 * wrap/python/cgi/ltl2tgba.in: Typos. Alexandre Duret-Lutz 2004-05-25 09:03:51 +00:00
• 2b1efe172c * wrap/python/cgi/ltl2tgba.in: Typos. Alexandre Duret-Lutz 2004-05-25 08:56:16 +00:00
• 1245d19d23 * src/sanity/style.test: Catch `;'-not-followed-by-space. * src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style. Alexandre Duret-Lutz 2004-05-24 18:16:27 +00:00
• 0e0fd18ca3 * src/ltlvisit/reducform.hh: Fix some Doxygen comments. Alexandre Duret-Lutz 2004-05-24 18:07:09 +00:00
• 57f6fcc40c * src/tgbatest/ltl2tgba.cc (syntax): Keep options sorted. Alexandre Duret-Lutz 2004-05-24 17:47:00 +00:00
• 9d375915f7 * src/sanity/Makefile.am (EXTRA_DIST): Distribute 80columns.test and style.test. Alexandre Duret-Lutz 2004-05-24 15:13:36 +00:00
• a37bac0133 * src/ltltest/Makefile.am (EXTRA_DIST): Distribute formulae.txt. * src/ltltest/formulae.txt: New files (2200 LTL formulea generated by Wring). * src/ltltest/formules.ltl: Delete. * src/reduc.test: Read formulae.txt. Alexandre Duret-Lutz 2004-05-24 12:59:34 +00:00
• 57fa1c8b5f * iface/gspn/ssp.hh (gspn_ssp_interface::gspn_ssp_interface): Add the `inclusion' flag. * iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call inclusion_version when inclusion is set. * iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3, -e4, and -e5. Alexandre Duret-Lutz 2004-05-24 11:53:57 +00:00
• f27b91c7d7 * iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop, and dead_prop from the dead argument passed to the constructor. (tgba_succ_iterator_gspn): Stutter on dead transitions. (tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_. (gspn_interface::gspn_interface): Hand dead to tgba_gspn. * iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a dead argument. * iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the dead property. * iface/gspn/udcseltl.test: Try option -d. Alexandre Duret-Lutz 2004-05-21 13:54:38 +00:00
• 3e968a3c9d * src/sanity/style.test: Check the iface/ tree too. * iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style. Alexandre Duret-Lutz 2004-05-21 11:55:36 +00:00
• da2d2e19b1 * src/sanity/80columns.test: Check the iface/ tree too. * iface/gspn/dcswaveltl.test, iface/gspn/dcswavefm.test, iface/gspn/dcswaveeltl.test, iface/gspn/udcsltl.test, iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, iface/gspn/udcsefm.test: Wrap to fit 80 columns. Alexandre Duret-Lutz 2004-05-21 11:46:22 +00:00
• 9329ea177d remove from CVS since Automake installs it Alexandre Duret-Lutz 2004-05-18 09:24:04 +00:00
• 9c0b0c53e6 * doc/Makefile.am (EXTRA_DIST, spot.html): Built the html documentation in $(srcdir) since it is distributed. * doc/Doxyfile.in (HTML_OUTPUT): Likewise. Upgrade to Doxygen 1.3.7. Alexandre Duret-Lutz 2004-05-18 09:21:25 +00:00
• 62a05ab1fb * src/ltlvisit/basereduc.cc, src/ltltest/inf.cc (main): Style. martinez 2004-05-17 15:17:55 +00:00
• 788ed772c2 * src/ltlvisit/basereduc.cc (spot): 80 columns. * src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc, src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh, src/tgbatest/ltl2tgba.cc (main): More option. * src/ltltest/inf.test: More test. martinez 2004-05-17 14:50:17 +00:00
• 41589e2818 * wrap/python/buddy.i: Define typemap for input_buf and use it for fdd_extdomain. Define const_int_ptr and use it for fdd_vars. Alexandre Duret-Lutz 2004-05-17 13:18:32 +00:00
• 7f1d5f597c * src/misc/bddalloc.cc (bdd_allocator::varnum): Suppress. (bdd_allocator::bdd_allocator): Adjust. (bdd_allocator::extvarnum): Always call bdd_varnum(), so that it doesn't matter if the number of variable has been augmented externally. * src/misc/bddalloc.hh (bdd_allocator::varnum): Suppress. Alexandre Duret-Lutz 2004-05-17 13:17:13 +00:00
• eccfdc6c1e * src/ltlvisit/formlength.cc: Fix style to please sanity checks. Alexandre Duret-Lutz 2004-05-17 10:56:31 +00:00
• cfcfb6d425 * src/ltlvisit/lunabbrev.cc: Fix style to please sanity checks. Alexandre Duret-Lutz 2004-05-17 10:52:48 +00:00
• 25dc63d1d4 * src/tgbaalgos/neverclaim.cc: Fix them. * sanity/style.test: Diagnose semicolons with leading spaces. Alexandre Duret-Lutz 2004-05-17 10:33:46 +00:00
• d22c647322 * src/ltlvisit/forminf.cc: Fix style to please sanity checks. Also avoid node_type_form_visitor where a dynamic_cast is done. Alexandre Duret-Lutz 2004-05-17 10:28:55 +00:00
• 1e2669d640 * wrap/python/buddy.i: Preliminary bindings for FDD and BVEC. Alexandre Duret-Lutz 2004-05-14 16:11:46 +00:00
• f2f10852c6 * ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style. * sanity/style.test: More tests. Alexandre Duret-Lutz 2004-05-14 14:09:01 +00:00
• aa5368baf9 * src/tgbatest/ltl2tgba.cc (main): Fix style. * HACKING: Mention `else if'. Alexandre Duret-Lutz 2004-05-14 13:21:32 +00:00
• 16fd8268c4 * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Do not output space before colon, and do not output the top-level formula using Spin's syntax. Alexandre Duret-Lutz 2004-05-14 13:12:02 +00:00
• 30652ba336 * src/tgbatest/ltl2tgba.cc (main): Thinko. martinez 2004-05-14 13:08:26 +00:00
• 9db2b31484 * src/ltlvisit/basereduc.cc (spot): Correct some mistakes. * src/ltlvisit/lunabbrev.cc (spot): Nothing change. * src/tgbatest/ltl2tgba.cc (main): More option to reduce formula. * src/tgbatest/spotlbtt.test: One more test. martinez 2004-05-14 12:55:13 +00:00
• 35ef738ff9 * src/ltlvisit/tostring.cc (to_spin_string_visitor, to_string_visitor): Do not parenthesize the top-level formula. * tgbatest/explicit.test, tgbatest/explpro2.test, tgbatest/explpro3.test, tgbatest/explprod.test, tgbatest/readsave.test, tgbatest/tgbaread.test, tgbatest/tripprod.test: Adjust expected output. * sanity/style.test: Fix regexes to catch an error seen in tostring.cc. Alexandre Duret-Lutz 2004-05-14 11:01:14 +00:00
• 6f4ab3af6c * src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component): Do not try to erase state that are not found in H. Report from Soheib Baarir. Alexandre Duret-Lutz 2004-05-14 09:05:17 +00:00
• 0c44ca35b3 * src/ltltest/reduc.test: Use ./defs and clean result.data. * src/ltltest/Makefile.am (CLEANFILES): Clean result.data. Alexandre Duret-Lutz 2004-05-14 08:41:32 +00:00
• 4cd10c3dfc * src/ltlvisit/Makefile.am: Copyright 2004. * src/ltltest/inf.test: More test. * src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot): Use dynamic_cast. * src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh, src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option to choose which rules applies to simplify the formula. martinez 2004-05-13 16:00:15 +00:00
• f7e5fe0821 * src/ltltest/reduc.test: Typo. Alexandre Duret-Lutz 2004-05-13 09:50:48 +00:00
• 60a3b4ed72 * src/ltlparse/ltlparse.yy (OP_POST_NEG, OP_POST_POS): New tokens. (subformula): Recognize ATOMIC_PROP OP_POST_POS' and ATOMIC_PROP OP_POST_NEG'. * src/ltlparse/ltlscan.ll: Introduce the not_prop start condition, to restrict the set of atomic propositions allowed in places where they are not expected. Make true' and false' case insensitive. * src/ltltest/parse.test, src/ltltest/tostring.test: More cases. * src/ltlvisit/tostring.cc (to_string_visitor): Quote atomic propositions equal to "true" or "false". Alexandre Duret-Lutz 2004-05-13 09:49:06 +00:00
• 4f96a9fc14 * src/ltltest/Makefile.am (TESTS): Run inf.test and reduc.test last. Alexandre Duret-Lutz 2004-05-11 11:03:22 +00:00
• a66e7250bf * src/ltltest/reduc.test: POSIXify. Alexandre Duret-Lutz 2004-05-11 08:51:20 +00:00
• c4a5b325a2 * src/sanity/style.test: New file. * src/sanity/Makefile.am (check-local): Run it. * src/ltlvisit/nenoform.cc, src/ltlvisit/tostring.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc, src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/lbtt.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/reachiter.cc, src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc, src/tgbatest/ltl2tgba.cc: Fix style issues reported by style.test. Alexandre Duret-Lutz 2004-05-10 18:38:20 +00:00
• 69169970a2 * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test, src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh: Fix copyright year, these files were created in 2004. Alexandre Duret-Lutz 2004-05-10 17:26:32 +00:00
• 83de4264cb * src/sanity/80columns.test: New file. * src/sanity/Makefile.am (check-local): Run it. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parseerr.test src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test, src/tgbatest/tripprod.test: Wrap long lines. Alexandre Duret-Lutz 2004-05-10 17:18:27 +00:00
• e69d0fa94e * src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula. martinez 2004-05-10 17:07:21 +00:00
• acb454fe6c reverse mistaken commit martinez 2004-05-10 16:43:30 +00:00
• 61e7d4e21f * src/ltltest/formules.ltl: A pattern of 2000 formulas. * src/ltltest/inf.test: Test some case of implies. * src/ltltest/inf.cc: Test some case of implies. * src/ltltest/reduc.test: Test reduction of a file of formula. * src/ltltest/reduc.cc: Test reduction of a formula. martinez 2004-05-10 16:40:34 +00:00
• bafc92d0b8 *** empty log message *** martinez 2004-05-10 15:43:18 +00:00
• faf4a2af26 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine fair_loop_approximation when branching postponement is not used. Alexandre Duret-Lutz 2004-05-10 13:43:22 +00:00
• 040f8beec7 Cache formula translations, and canonize formulae before doing branching postponement. * src/tgbaalgos/ltl2tgba_fm.cc (formula_canonizer): New class, with bits extracted from fill_dests and ltl_to_tgba_fm. (fill_dests, ltl_to_tgba_fm): Adjust to use formula_canonizer. Alexandre Duret-Lutz 2004-05-10 12:17:07 +00:00
• aa5cef3c83 * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument fair_loop_approx. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Implement the fair_loop_approx optimization. (ltl_promise_visitor, ltl_possible_fair_loop_visitor, possible_fair_loop_checker): New classes. * src/tgbatest/ltl2tgba.cc: Add the -L option. * src/tgbatest/spotlbtt.test: Exercise fair_loop_approx. * wrap/python/cgi/ltl2tgba.in: Make it an option. Alexandre Duret-Lutz 2004-05-10 10:41:28 +00:00
• 6b06e28f3d * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add argument branching_postponement. * src/tgbaalgos/ltl2tgba_fm.cc (fill_dests): New function, extracted from ltl_to_tgba_fm(). (ltl_to_tgba_fm): Implement the branching_postponement optimization. * src/tgbatest/ltl2tgba.cc: Add the -p option. * src/tgbatest/spotlbtt.test: Exercise branching postponement. * wrap/python/cgi/ltl2tgba.in: Make it an option. Alexandre Duret-Lutz 2004-05-07 10:00:34 +00:00
• f11df7679a * src/tgbaalgos/ltl2tgba_fm.cc: Add a superfluous return to pacify some GCC version. Report from Denis Poitrenaud. Alexandre Duret-Lutz 2004-05-04 11:22:06 +00:00
• b052e92537 * wrap/python/cgi/ltl2tgba.in: Fix output HTML. Alexandre Duret-Lutz 2004-05-04 07:33:12 +00:00
• ca80561ad5 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Clone and then free all formulae entered into canonical_succ, to avoid errors when a formula is entered into canonical_succ but not into formulae_seen. * src/tgbatest/ltl2tgba.test: Add a new test, and check with -f. Report from Thomas Martinez. Alexandre Duret-Lutz 2004-05-03 16:41:00 +00:00
• 22912b6db7 * configure.ac, NEWS: Bump version to 0.0u. Alexandre Duret-Lutz 2004-04-23 17:54:02 +00:00
• b980717756 * configure.ac, NEWS: Bump version to 0.0t. * HACKING: Update tools requirements. * src/sanity/Makefile.am (EXTRA_DIST): Distribute includes.test. Alexandre Duret-Lutz 2004-04-23 17:31:57 +00:00
• 007143e9e3 * src/sanity/Makefile.am, src/sanity/includes.test: New files. * src/Makefile.am (SUBDIRS): Add sanity. * configure.ac: Output src/sanity/Makefile.in. Alexandre Duret-Lutz 2004-04-23 12:27:40 +00:00
• 7cf55415a7 * src/tgbatest/Makefile.am (check_PROGRAMS): Move ltl2tgba ... (noinst_PROGRAMS): ... here. * iface/gspn/Makefile.am (check_PROGRAMS): Rename as ... (noinst_PROGRAMS): ... this. Alexandre Duret-Lutz 2004-04-23 11:27:21 +00:00
• 70e93ea053 * src/tgbatest/explicit.test: Reorder bdd variable in output. Report from Denis Poitrenaud. Alexandre Duret-Lutz 2004-04-22 12:02:53 +00:00
• 28288e0478 * wrap/python/cgi/ltl2tgba.in: Print degeneralized statistics when show_never_claim. Change the title to LTL-to-TGBA. Alexandre Duret-Lutz 2004-04-22 10:13:10 +00:00
• d07e549832 * wrap/python/cgi/ltl2tgba.in (print_footer): Make ltl2tgba.py's version a separate variable. Alexandre Duret-Lutz 2004-04-21 21:03:56 +00:00
• 9a8d554f59 * wrap/python/cgi/ltl2tgba.in: Pass the formula to never_claim_reachable, and cgi.escape its output. Lighten the color a bit. Alexandre Duret-Lutz 2004-04-21 20:23:57 +00:00
• cf1ab2946f * src/tgbaalgos/gtec/ce.hh, src/misc/freelist.hh, src/tgba/bddprint.hh: Fix Doxygen comments. Alexandre Duret-Lutz 2004-04-21 20:14:40 +00:00
• 2f84bee41c * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document arguments. * src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting): New method. (never_claim_bfs::get_state_label, never_claim_bfs::process_state): Use it. Alexandre Duret-Lutz 2004-04-21 20:08:36 +00:00
• 231a77a05f * wrap/python/cgi/ltl2tgba.in: Use darker color and introduce the new variable dot_bgcolor. Alexandre Duret-Lutz 2004-04-21 19:52:30 +00:00
• 5904255b14 * wrap/python/cgi/ltl2tgba.in (add_options): Revamp options output using this new function. Alexandre Duret-Lutz 2004-04-21 19:32:37 +00:00
• 0c3d4fef9f * wrap/python/spot.i: Process tgbaalgos/neverclaim.hh. * wrap/python/cgi/ltl2tgba.in: Display the never claim on demand. Alexandre Duret-Lutz 2004-04-21 19:02:31 +00:00
• 8d8af2e53a * src/ltlvisit/tostring.hh (to_spin_string): New function. Convert a formula into a string parsable by Spin. * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files. Print the never claim in Spin format of a degeneralized TGBA. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the never claim in Spin format of a degeneralized TGBA. * src/tgbatest/ltl2neverclaim.test: New file. * src/tgbatest/Makefile.am: Add it. Alexandre Duret-Lutz 2004-04-21 15:18:07 +00:00
• 4d73490a49 * src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode when valgrind is not used. Reported by Denis Poitrenaud. Alexandre Duret-Lutz 2004-04-20 11:11:40 +00:00
• 00487e1176 * src/tgba/tgba.hh (tgba::succ_iter): Doco. * src/tgba/tgbatba.hh (tgba_tba_proxy::state_is_accepting): Document it. Reported by Denis Poitrenaud. Alexandre Duret-Lutz 2004-04-20 09:36:49 +00:00
• ed53965347 * iface/gspn/ltlgspn.cc (main) [SSP]: Use the standard counter-example computation for -e5 too. Alexandre Duret-Lutz 2004-04-17 13:37:58 +00:00
• 83c4c02d35 * iface/gspn/ltlgspn.cc (main) [!SSP]: Do not accept -e3, -e4, or -e5. (main) [SSP]: Use the standard counter-example computation for -e and -e1. Alexandre Duret-Lutz 2004-04-16 22:05:14 +00:00
• 133bcf9442 Rename EESRG as SSP. * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/dottyeesrg.cc: Rename as ... * iface/gspn/ssp.cc, iface/gspn/ssp.hh, iface/gspn/dottyssp.cc: ... these. Adjust all classes and function names. * iface/gspn/ltlgspn.cc, iface/gspn/Makefile.am: Adjust all classes filenames and function names. * m4/gspnlib.m4: Define WITH_GSPN_SSP and LIBGSPNSSP_LDFLAGS. Alexandre Duret-Lutz 2004-04-15 12:05:20 +00:00
• 8ff4ca08ce * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map::find): Rewrite. (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_hash_map::index): New functions. (numbered_state_heap_hash_map::filter): Delete. * iface/gspn/eesrg.cc (numbered_state_heap_eesrg_semi::find, numbered_state_heap_eesrg_semi::index): Rewrite. (numbered_state_heap_eesrg_semi::filter): Remove. * src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/ce.cc: Adjust to use find() and index() instead of filter().. Alexandre Duret-Lutz 2004-04-15 11:50:29 +00:00
• be4f4e3370 * iface/gspn/eesrg.cc (connected_component_eesrg::has_state): Free filtered states. (emptiness_check_shy_eesrg): New class. (emptiness_check_eesrg_shy): New function. * iface/gspn/eesrg.hh (emptiness_check_eesrg_shy): New function. * iface/gspn/ltlgspn.cc (main) [EESRG]: Handle -e3, -e4, and -e5. * * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc (emptiness_check_shy::check): Move arc, num, succ_queue, and todo as attributes. (emptiness_check_shy::find_state): New virtual function. Alexandre Duret-Lutz 2004-04-15 09:12:11 +00:00
• 1e360ec689 * iface/gspn/ltlgspn.cc (connected_component_eesrg, connected_component_eesrg_factory, numbered_state_heap_eesrg_semi, numbered_state_heap_eesrg_const_iterator, numbered_state_heap_eesrg_factory_semi): New classes. (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/eesrg.hh (emptiness_check_eesrg_semi, emptiness_check_eesrg_shy_semi, counter_example_eesrg): New functions. * iface/gspn/ltlgspn.cc [EESRG]: Adjust to call these new functions. Alexandre Duret-Lutz 2004-04-14 15:20:35 +00:00