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

Commit graph

  • 7da112344e Remove `readsave' and fix line numbers in tgbaparse error messages. Alexandre Duret-Lutz 2010-11-06 14:14:18 +01:00
  • a53706c824 * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.5. Alexandre Duret-Lutz 2010-11-06 09:20:03 +01:00
  • b240bd8204 * configure.ac: Do not run CF_GXX_WARNINGS unless they are enabled. Alexandre Duret-Lutz 2010-10-07 15:29:28 +02:00
  • 1fa1621a6b Hide the safra_tree_automaton type from the public interface. Alexandre Duret-Lutz 2010-10-07 15:17:18 +02:00
  • 498b44f742 Revert "Add never claim parser." Alexandre Duret-Lutz 2010-06-21 17:41:20 +02:00
  • 9aaa638b27 Add never claim parser. Felix Abecassis 2010-05-25 16:19:20 +02:00
  • be6efe94a4 Fix the --enable-optimizations check. Alexandre Duret-Lutz 2010-05-20 17:16:59 +02:00
  • c9dd3f86b4 * NEWS: Typo. Alexandre Duret-Lutz 2010-04-16 13:45:03 +02:00
  • e084e06f43 * NEWS, configure.ac: Bump version to 0.6a. Alexandre Duret-Lutz 2010-04-16 10:29:43 +02:00
  • 02d01257ed Release Spot 0.6. Alexandre Duret-Lutz 2010-04-16 09:39:52 +02:00
  • ce51ed3002 Reorder recent additions to reduccmp.test. Alexandre Duret-Lutz 2010-04-15 19:05:03 +02:00
  • 5755a531f9 Fix a long-standing bug in the stronger rule for R and its recent clone for M. Alexandre Duret-Lutz 2010-04-15 14:57:19 +02:00
  • 1a91208933 More simplifications rules for M. Alexandre Duret-Lutz 2010-04-15 13:01:21 +02:00
  • 946f305f7c Speed up syntactic_implication() for constants. Alexandre Duret-Lutz 2010-04-15 12:27:31 +02:00
  • 7021e45f70 Fix simplification of "a M true" as Fa. Alexandre Duret-Lutz 2010-04-15 11:44:17 +02:00
  • 9a1769fe78 * HACKING: Bison 2.4.2 has a bugfix we rely on. Alexandre Duret-Lutz 2010-04-15 10:59:26 +02:00
  • 70669c99ed * src/tgbatest/ltl2tgba.cc (syntax): Add missing black line in help output. Alexandre Duret-Lutz 2010-04-15 09:46:18 +02:00
  • 26bd137020 * NEWS: Mention W and M. Alexandre Duret-Lutz 2010-04-14 18:58:40 +02:00
  • 28094c87da More LTL reductions for W and M. Alexandre Duret-Lutz 2010-04-14 18:46:04 +02:00
  • aa5426b2fb * wrap/python/cgi-bin/ltl2tgba.in: Document W and M operators. Alexandre Duret-Lutz 2010-04-12 16:10:45 +02:00
  • e6809b8c66 More LTL reductions for W and M. Alexandre Duret-Lutz 2010-04-12 15:26:48 +02:00
  • f003c3d16f Add LTL reductions for strong release. Alexandre Duret-Lutz 2010-04-12 13:39:28 +02:00
  • 80ceca599c Add LTL reductions for weak until. Alexandre Duret-Lutz 2010-04-12 12:19:33 +02:00
  • 0fc0ea3166 Add support for W (weak until) and M (strong release) operators. Alexandre Duret-Lutz 2010-04-07 10:44:07 +02:00
  • 35a57c6dff [lbtt] Accept W and M in lbtt-translate --spot. Alexandre Duret-Lutz 2010-04-07 10:26:19 +02:00
  • 60dbeb1128 Adjust ltl2tgba.py to call scc_filter() with the "full" option as appropriate. Alexandre Duret-Lutz 2010-04-12 16:39:28 +02:00
  • ef3c82e1b0 * src/ltlvisit/basicreduce.cc: Typo in comment. Alexandre Duret-Lutz 2010-04-08 15:56:58 +02:00
  • f282338e1c * NEWS: Summarize recent noteworthy changes. Alexandre Duret-Lutz 2010-04-08 15:41:42 +02:00
  • bbd526ac81 Modernize Bison parsers. Alexandre Duret-Lutz 2010-04-07 16:47:40 +02:00
  • d71ceb3b04 Fix column in LTL error messages, it was off by one. Alexandre Duret-Lutz 2010-03-10 15:17:05 +01:00
  • 3cf2ddbcb0 Do not rewrite F(a & GF(b)) = F(a) & GF(b), this can be harmful. Alexandre Duret-Lutz 2010-03-06 19:28:39 +01:00
  • 629dc4c0c9 * src/tgba/tgbatba.cc: Fix English in comments. Alexandre Duret-Lutz 2010-03-06 18:07:46 +01:00
  • 58b233db6f Reverse the order of expected acceptance conditions in degeneralization. Alexandre Duret-Lutz 2010-03-06 17:42:48 +01:00
  • 351a8076d0 Tweak precedence of "->" and <->. Alexandre Duret-Lutz 2010-03-06 17:39:42 +01:00
  • cc66aff634 * bench/ltl2tgba/formulae.ltl: Fix three formulae to match the original paper by Somenzi and Bloem. Reported by Ruediger Ehlers. Alexandre Duret-Lutz 2010-03-06 10:48:35 +01:00
  • 975045a4e6 Fix memory leak introduced in yesterday's change. Alexandre Duret-Lutz 2010-03-06 09:18:10 +01:00
  • 27b419ce17 Keep acceptance conditions on transitions going to accepting SCCs by default in scc_filter(). Alexandre Duret-Lutz 2010-03-06 00:18:33 +01:00
  • 2140256004 Simplify F(a)|F(b) as F(a|b). Add similar rule for G(a)&G(b). Alexandre Duret-Lutz 2010-03-05 23:16:01 +01:00
  • 34af32879c Better selection of the acceptance of the initial state in SBA. Alexandre Duret-Lutz 2010-03-05 22:35:18 +01:00
  • 52faa81a77 Generalize the previous patch to accepting states in SBA. Alexandre Duret-Lutz 2010-03-05 22:27:36 +01:00
  • 8405838347 lrde-upload.sh: Add support for git branches Alexandre Duret-Lutz 2010-03-03 12:32:21 +01:00
  • 96cc3a3f67 Optimize tgba_tba_proxy and tgba_sba_proxy for states that share an acceptance condition on all outgoing transitions. Alexandre Duret-Lutz 2010-03-03 10:52:38 +01:00
  • efb15a9171 ltl2tgba: apply -R3 before -D or -DS. Alexandre Duret-Lutz 2010-03-03 08:40:21 +01:00
  • 2598f794d8 * src/sanity/style.test: Better fix for the previous error. Alexandre Duret-Lutz 2010-02-24 13:56:08 +01:00
  • 57d5eb3cb3 Work around a spurious style.test error. Alexandre Duret-Lutz 2010-02-23 17:31:39 +01:00
  • 2183276008 Fix random_graph() not to generate dead states. Alexandre Duret-Lutz 2010-02-23 17:20:59 +01:00
  • 72b7deec12 ltl2tgba cgi updates. Alexandre Duret-Lutz 2010-02-08 10:18:36 +01:00
  • bc61ca73c6 * wrap/python/cgi-bin/ltl2tgba.in: Reword description of svg_output. Alexandre Duret-Lutz 2010-02-02 18:28:13 +01:00
  • 72ae820b0c Add SVG output and language containment options to the cgi script. Alexandre Duret-Lutz 2010-02-02 16:58:14 +01:00
  • a13ded583b * NEWS: Typo. Alexandre Duret-Lutz 2010-02-02 16:23:20 +01:00
  • e800eb185a * NEWS, configure.ac: Bump version to 0.5a. Alexandre Duret-Lutz 2010-02-01 10:37:09 +01:00
  • 0728b38cdd Release Spot 0.5. Alexandre Duret-Lutz 2010-02-01 10:08:40 +01:00
  • ca1bec3093 * doc/Makefile.am ($(srcdir)/stamp): Do not depend on dot explicitly, otherwise the documentation is always built and distcheck fails. Alexandre Duret-Lutz 2010-01-31 21:48:29 +01:00
  • 34728dca52 More Doxygen fixes. Alexandre Duret-Lutz 2010-01-31 20:57:02 +01:00
  • 5b87fa628d Build doxygen pictures with libgd to reduce their size. Alexandre Duret-Lutz 2010-01-31 18:47:41 +01:00
  • c63923fa1a More Doxygen fixes. Alexandre Duret-Lutz 2010-01-31 18:30:21 +01:00
  • 772c92fc9c * bench/split-product/Makefile.am (nodist_noinst_DATA): Do not depend on files that cannot be built. Alexandre Duret-Lutz 2010-01-30 17:33:35 +01:00
  • c1ec2383b9 more files to ignore Alexandre Duret-Lutz 2010-01-30 17:32:46 +01:00
  • 4ff875f402 Replace spot::ltl_file by a rewritten spot::ltl::ltl_file. Alexandre Duret-Lutz 2010-01-30 17:31:34 +01:00
  • dd3ac6b4f3 Check for missing Copyright blurbs, and add them. Alexandre Duret-Lutz 2010-01-30 16:32:13 +01:00
  • 91fee65a89 * NEWS: More text. Alexandre Duret-Lutz 2010-01-30 16:03:47 +01:00
  • dac0502706 Touch up some doxygen comments and copyrights. Alexandre Duret-Lutz 2010-01-30 16:00:37 +01:00
  • a4766f2f82 Add SCC pruning options to the CGI script. Alexandre Duret-Lutz 2010-01-30 14:52:16 +01:00
  • 322e1a0179 * src/evtgbatest/ltl2evtgba.test: Replace * by &. Alexandre Duret-Lutz 2010-01-30 14:16:15 +01:00
  • 4efde0d3d3 Make it possible to use the cgi script without installing a web server. Alexandre Duret-Lutz 2010-01-30 14:15:03 +01:00
  • 24cde3c21f More * -> & replacements. Alexandre Duret-Lutz 2010-01-30 13:21:01 +01:00
  • dd71e37df2 Remove the theoretically bogus "containment" option of ltl2tgba_fm. Alexandre Duret-Lutz 2010-01-30 12:26:45 +01:00
  • 7cc2776d91 * src/tgba/tgbasafracomplement.hh: Add missing copyright and fix some comments. Alexandre Duret-Lutz 2010-01-30 12:02:35 +01:00
  • 7647ba0fdd Rename tgba_complement as tgba_kv_complement. Alexandre Duret-Lutz 2010-01-30 11:56:45 +01:00
  • 85532dc8f8 Do not recognize "*" as "and". This leaves room for an implementation of rational operators in a future version. Alexandre Duret-Lutz 2010-01-30 11:41:31 +01:00
  • 55b693e123 Make Couvreur/FM the default translation. Alexandre Duret-Lutz 2010-01-30 11:20:27 +01:00
  • 369e4c419b Overhaul LaCIM's ELTL options. Alexandre Duret-Lutz 2010-01-30 11:15:51 +01:00
  • 9a43a06b45 Touch up -R3b handling. Alexandre Duret-Lutz 2010-01-30 09:46:46 +01:00
  • c00a80a2fc Update some text files for upcoming 0.5. Alexandre Duret-Lutz 2010-01-29 18:18:25 +01:00
  • 7d5f493fb2 Rename wrap/python/cgi/ as wrap/python/cgi-bin/. Alexandre Duret-Lutz 2010-01-29 15:19:25 +01:00
  • 28289f95b5 * src/tgbaalgos/gtec/gtec.hh: Fix copyright. Alexandre Duret-Lutz 2010-01-29 14:58:32 +01:00
  • f83e0d7a10 * src/tgbaalgos/ltl2tgba_fm.cc: More comments. Alexandre Duret-Lutz 2010-01-24 18:25:35 +01:00
  • 1fbdf0bcaf * src/tgba/taatgba.cc, src/tgba/taatbga.hh: Fix a memory issue on Darwin. Felix Abecassis 2010-01-29 15:26:39 +01:00
  • 58d6b7912c * wrap/python/cgi/ltl2tgba.in, wrap/python/spot.i: Add a new translation algorithm: Tauriainen/TAA. Damien Lefortier 2010-01-25 18:30:33 +01:00
  • d9b8fcddd6 * wrap/python/cgi/ltl2tgba.in: Use the uuid Python module instead of the UNIQUE_ID environment variable to avoid being Apache-specific. Damien Lefortier 2010-01-25 14:14:27 +01:00
  • 3a974d61f0 Fix copyrights. Guillaume Sadegh 2010-01-24 19:03:04 +01:00
  • 06f0fe1d40 Check that all directories are documented. Alexandre Duret-Lutz 2010-01-24 14:56:43 +01:00
  • 9f41e397d5 * README: Typo. Alexandre Duret-Lutz 2010-01-24 11:53:35 +01:00
  • ec2e54df81 * src/sanity/Makefile.am (EXTRA_DIST): Distribute readme.test. Alexandre Duret-Lutz 2010-01-24 10:41:07 +01:00
  • 2919b64532 * README: Add descriptions for subdirectories of bench/, src/sanity, and src/kripke. Alexandre Duret-Lutz 2010-01-24 10:37:07 +01:00
  • cbdb0feb68 * src/sanity/readme.test: A script to check whether all the directories referenced in README exist. * src/sanity/Makefile.am: Adjust to call `readme.test' when make check is invoked. Guillaume Sadegh 2010-01-24 03:06:00 +01:00
  • 3633fced1d Update the README. Guillaume Sadegh 2010-01-24 02:42:38 +01:00
  • 1693e2afad more files to ignore Alexandre Duret-Lutz 2010-01-22 17:31:42 +01:00
  • 391372ae2a Turn parse_error_list into an opaque type for Swig. This kills a memory leak warning from swig/python. Alexandre Duret-Lutz 2010-01-22 17:29:12 +01:00
  • 0fe5403956 Revert inlining of bdd_addref() and bdd_delref(). Alexandre Duret-Lutz 2010-01-22 15:55:08 +01:00
  • 9cbaae7b66 [lbtt] Let "make dvi" work on Ubuntu. Alexandre Duret-Lutz 2010-01-22 13:14:48 +01:00
  • e828783f47 [buddy] Get rid of some "deprecated conversion from string constant to `char*'" warnings. Alexandre Duret-Lutz 2010-01-22 11:13:46 +01:00
  • 919fc298ff Fix the computation of the length of multops. Alexandre Duret-Lutz 2010-01-22 11:00:49 +01:00
  • e733f951be Please the style checks... Alexandre Duret-Lutz 2010-01-21 22:09:10 +01:00
  • 38a1fadaa0 * src/ltltest/reduc.cc (main): Fix harmless memory leak introduced today. Alexandre Duret-Lutz 2010-01-21 16:56:44 +01:00
  • bfadcf8021 [iface/nips/nips_vm] Kill a warning on Ubuntu. Alexandre Duret-Lutz 2010-01-21 16:00:10 +01:00
  • a6b9583628 [lbtt] Kill some warnings on Ubuntu. Alexandre Duret-Lutz 2010-01-21 15:58:18 +01:00
  • e20ba143bb [buddy] * src/bddio.c (bdd_load): Check the return value of fscanf() to kill a warning. Alexandre Duret-Lutz 2010-01-21 15:51:23 +01:00
  • e663c222e5 Fix taa_tgba_formula's destructor. Alexandre Duret-Lutz 2010-01-21 15:16:43 +01:00
  • eef27f4496 * src/tgbatest/randtgba.cc: Do not include <string> twice. Alexandre Duret-Lutz 2010-01-21 14:55:01 +01:00