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

Commit graph

  • b98c47246c [buddy] Adjust parser construction to support Automake 1.11 and 1.12. Alexandre Duret-Lutz 2012-06-19 17:03:34 +02:00
  • 25aca9ab7a Fix a few files that claimed to be distributed under GPLv3 by mistake. Alexandre Duret-Lutz 2012-06-19 16:22:43 +02:00
  • 9460e0761e FM: Translate X(a&b) as if it were X(a)&X(b). Alexandre Duret-Lutz 2012-06-18 18:25:07 +02:00
  • d7ff066513 Fix computation of support_conditions in tgba_wdba_comp_proxy. Alexandre Duret-Lutz 2012-06-07 22:34:00 +02:00
  • 03b13891e3 * bench/ltl2tgba/algorithms: Add two missing degeneralized config. Alexandre Duret-Lutz 2012-06-06 21:57:37 +02:00
  • cec5b3f41e * bench/ltlclasses/README: Fix a typo. Thomas Badie 2012-06-06 15:51:28 +02:00
  • fdbdb1a436 Fix a memory leak on failure to WDBA-minimize. Alexandre Duret-Lutz 2012-06-06 10:40:16 +02:00
  • fddfafcd60 * doc/tl/tl.tex: Typos. Alexandre Duret-Lutz 2012-06-05 18:10:13 +02:00
  • 57ec1c61c9 * doc/mainpage.dox: Use a better title. Alexandre Duret-Lutz 2012-06-02 12:31:47 +02:00
  • 7b7a946485 Rework the timeout of the CGI script. Alexandre Duret-Lutz 2012-06-04 16:38:42 +02:00
  • 75862a3284 * doc/tl/tl.tex: Add a tricky example for the {r} operator. Alexandre Duret-Lutz 2012-06-04 15:47:40 +02:00
  • 87765ca8e8 * doc/tl/tl.tex: Remarks from Denis Poitrenaud. Alexandre Duret-Lutz 2012-06-04 15:43:03 +02:00
  • f620d9a231 * NEWS, configure.ac: Bump version to 0.9.1a. Alexandre Duret-Lutz 2012-05-23 13:19:30 +02:00
  • 669d796eb4 Release Spot 0.9.1 Alexandre Duret-Lutz 2012-05-23 12:02:37 +02:00
  • 9559799637 Export tgba_parse() to the python interface. Alexandre Duret-Lutz 2012-05-23 11:47:12 +02:00
  • ebf4d2585d Make it easier to convert acc-conditions to associated formulae. Alexandre Duret-Lutz 2012-05-22 17:57:12 +02:00
  • 8893f34da1 * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2012-05-22 13:43:34 +02:00
  • 72f36c50a5 Clear the contaiment cache after -r7. Alexandre Duret-Lutz 2012-05-21 22:35:51 +02:00
  • 1c1c95f65f Use the distributed LBTT is the installed one is not 1.2.1a. Alexandre Duret-Lutz 2012-05-21 14:36:30 +02:00
  • a8fd9e8b14 [lbtt] Make it clearer this is not LBTT 1.2.1. Alexandre Duret-Lutz 2012-05-21 14:35:03 +02:00
  • faed4e8be2 Adjust parseout.pl to the new LBTT output. Alexandre Duret-Lutz 2012-05-21 13:46:44 +02:00
  • f2b188d9ec [lbtt] Count deterministic automata and deterministic states. Tomáš Babiak 2012-05-21 12:16:33 +02:00
  • 31b3a22805 FM: Simplify promises of U, M, and F formulae. Alexandre Duret-Lutz 2012-05-20 12:43:02 +02:00
  • cb068599dc ltl2tgba: Set assume_sba for automata read from a neverclaim. Alexandre Duret-Lutz 2012-05-19 22:58:55 +02:00
  • e5a86290cf Clean the as_bdd() cache after LTL simplification. Alexandre Duret-Lutz 2012-05-19 22:51:18 +02:00
  • 9633dd6e88 Speedup syntactic implication by not comparing literals using bdd. Alexandre Duret-Lutz 2012-05-19 21:08:36 +02:00
  • a80a5137fd Add -rD option to ltl2tgba, to display some caching statistics. Alexandre Duret-Lutz 2012-05-19 21:03:56 +02:00
  • babc024097 Correctly handle ltl2tgba's option -rL. Alexandre Duret-Lutz 2012-05-19 00:11:13 +02:00
  • 8c454f9ddf FM: use a vector to store the Next BDD->formula map. Alexandre Duret-Lutz 2012-05-13 16:21:27 +02:00
  • 191fa370e2 Overhaul bdddict to speedup bdd->formula lookups. Alexandre Duret-Lutz 2012-05-13 14:25:59 +02:00
  • c5b294c786 FM: collect implied formulae in & arguments; do not to translate them Alexandre Duret-Lutz 2012-05-13 09:21:20 +02:00
  • 1b143067c0 Faster translation of GFa. Alexandre Duret-Lutz 2012-05-11 11:20:00 +02:00
  • e2f70e72b8 Fix translation of !{r}. Alexandre Duret-Lutz 2012-05-12 11:48:02 +02:00
  • 14144f3b3b * wrap/python/ajax/README: More debugging help. Alexandre Duret-Lutz 2012-05-11 23:35:49 +02:00
  • 2d0ac3eb75 * src/tgbaalgos/simulation.cc (get_state): Do not lookup the map twice. Alexandre Duret-Lutz 2012-05-10 21:45:03 +02:00
  • ebe2362bc9 Equip the LTL parser with printers for formulas and other token. Alexandre Duret-Lutz 2012-05-10 10:11:11 +02:00
  • 509edabab4 Missing space in help text. Alexandre Duret-Lutz 2012-05-10 10:09:58 +02:00
  • 9f127deae6 Fix generation of randome SERE formulae. Alexandre Duret-Lutz 2012-05-10 10:09:04 +02:00
  • de64a48e8b * m4/buddy.m4: Typo, reported by Thomas Badie. Alexandre Duret-Lutz 2012-05-09 21:49:20 +02:00
  • c18c153209 * configure.ac, NEWS: Bump version to 0.9a. Alexandre Duret-Lutz 2012-05-09 17:42:28 +02:00
  • 1e0ae54892 Release Spot 0.9 Alexandre Duret-Lutz 2012-05-09 13:19:35 +02:00
  • 2945668021 Update the help text for the Couvreur/FM algorithm. Alexandre Duret-Lutz 2012-05-09 13:15:46 +02:00
  • b71eadd8e3 Fix syntactic implication rule between R/M and U/W. Alexandre Duret-Lutz 2012-05-07 15:58:42 +02:00
  • 70e3e2cd04 * NEWS: Typo in date. Alexandre Duret-Lutz 2012-05-07 14:45:28 +02:00
  • b9afd8e705 Fix mismatch between srand/srand48 and rand/rand48. Alexandre Duret-Lutz 2012-05-07 14:36:54 +02:00
  • a2893520ca Properly thank Christian and Felix. Alexandre Duret-Lutz 2012-05-07 14:30:43 +02:00
  • 7438fa3c65 Fix LTL output for Spin. Alexandre Duret-Lutz 2012-05-05 11:05:58 +02:00
  • 927d745805 80columns.test: Add workaround for non-unicode systems. Alexandre Duret-Lutz 2012-05-03 20:46:59 +02:00
  • f5fea7484b Fix two formula leaks. Alexandre Duret-Lutz 2012-05-03 18:50:24 +02:00
  • 1f54581215 * src/tgba/tgbaexplicit.hh: Fix clang-3.0 warnings. Alexandre Duret-Lutz 2012-05-03 10:55:19 +02:00
  • 2c3df109e1 * src/tgbatest/ltl2tgba.cc (-rs): New option for reduce_size_striclty. Alexandre Duret-Lutz 2012-05-02 20:23:58 +02:00
  • 42963b99c8 Adjust benchmarks that had not been compiled since 0.8... Alexandre Duret-Lutz 2012-05-02 18:19:57 +02:00
  • db4693b303 Downcase a couple of misnamed class names. Alexandre Duret-Lutz 2012-05-02 17:57:38 +02:00
  • dadfbdad9d Small documentation fixes. Alexandre Duret-Lutz 2012-05-02 13:08:03 +02:00
  • 1a50ae3bf8 * src/ltlvisit/simplify.cc: Add missing call to recurse_destroy(). Alexandre Duret-Lutz 2012-05-02 12:06:23 +02:00
  • 4a9bbbafe2 Add ltl3ba to the ltl2tgba benchmark. Alexandre Duret-Lutz 2012-05-02 09:59:33 +02:00
  • bf62d439c9 Use 'const formula*' instead of 'formula*' everywhere. Alexandre Duret-Lutz 2012-05-01 23:38:55 +02:00
  • 0f0ada825a Show how to rewrite a̅ as ¬a before calling dot, if needed. Alexandre Duret-Lutz 2012-05-01 14:31:15 +02:00
  • ec08e5dce1 * doc/tl/tl.bib (babiak.12.tacas): Update reference. Alexandre Duret-Lutz 2012-04-30 19:38:58 +02:00
  • 861969b53a Prefer -R3 to -R3f when applying direct simulation in the web interface. Alexandre Duret-Lutz 2012-04-30 18:11:13 +02:00
  • fb6a2a50b5 One more test for U,W,R,M rewritins. Alexandre Duret-Lutz 2012-04-30 18:03:33 +02:00
  • 84cefea203 * src/tgbaalgos/minimize.hh: Reencode in utf-8 and wrap long lines. Alexandre Duret-Lutz 2012-04-30 16:13:13 +02:00
  • 6a250eb9c3 * doc/tl/tl.tex: Disable draft mode. Alexandre Duret-Lutz 2012-04-30 08:52:35 +02:00
  • a9cccd11e6 Change tgba_dupexp_bfs() and tgba_dupexp_dfs() to build numbered tgba. Alexandre Duret-Lutz 2012-04-20 14:21:13 +02:00
  • 0821599db8 Implement rewritings for {f|g} and !{f|g}. Alexandre Duret-Lutz 2012-04-29 23:36:12 +02:00
  • 496c449fa4 Update the intro of tl.tex, and add a reference to VECOS'11. Alexandre Duret-Lutz 2012-04-29 23:12:42 +02:00
  • 776564cbf2 Rertite a M (b | a) = b U a and a R (b | a) == b W a. Alexandre Duret-Lutz 2012-04-29 22:47:42 +02:00
  • a09ad6b4c6 Implement W,M removal for Spin output. Alexandre Duret-Lutz 2012-04-29 21:21:03 +02:00
  • e64a1bf565 * NEWS: Mention utf-8 output. Alexandre Duret-Lutz 2012-04-29 19:51:36 +02:00
  • 6ea88efddc Allow atomic propositions negated with a combining overline. Alexandre Duret-Lutz 2012-04-29 19:25:43 +02:00
  • 1319e18e1d Make sure PYTHON is absolute. Alexandre Duret-Lutz 2012-04-29 18:19:08 +02:00
  • 43d1be09d5 Add an UTF-8 option to the web interface. Alexandre Duret-Lutz 2012-04-29 16:44:50 +02:00
  • e93ceebafe Make it possible to output UTF-8 for dotty(). Alexandre Duret-Lutz 2012-04-29 01:15:08 +02:00
  • f082700fb2 Fix constness of minimize_wdba() return. Alexandre Duret-Lutz 2012-04-29 00:44:38 +02:00
  • df1785f526 Fix doxygen comments. Alexandre Duret-Lutz 2012-04-29 00:43:08 +02:00
  • 53f38c2ccd Implement to_utf8_string(). Alexandre Duret-Lutz 2012-04-29 00:40:27 +02:00
  • 6f29141174 Remove useless include. Alexandre Duret-Lutz 2012-04-28 22:56:44 +02:00
  • 5eae815a1c Document recognized utf8 characters. Alexandre Duret-Lutz 2012-04-28 21:02:43 +02:00
  • 7e4787da22 Fix error reporting in utf8-encoded LTL formulae. Alexandre Duret-Lutz 2012-03-29 14:14:56 +02:00
  • 403170f5c8 Distribute UTF8-for-cpp. Alexandre Duret-Lutz 2012-03-29 11:52:47 +02:00
  • 80a9c3e219 ltlparse: Preliminary support for utf8 operators. Alexandre Duret-Lutz 2012-03-14 18:56:33 +01:00
  • ce437cd499 Fix the associativity of ->, <->, U, R, W, and M wrt the PSL standard. Alexandre Duret-Lutz 2012-04-28 16:13:24 +02:00
  • 807dcefba4 Document the changes from the PSL branch. Alexandre Duret-Lutz 2012-04-28 10:55:02 +02:00
  • bdeb87a6b0 web ltl2tgba: add an option to disable larger rewritings Alexandre Duret-Lutz 2012-04-27 15:24:02 +02:00
  • 8f40fd41f4 Replace the "encoding: utf-8" by "coding: utf-8" comments. Alexandre Duret-Lutz 2012-04-27 09:14:17 +02:00
  • aec556f7a2 Implement basic rewriting rules for {r} and !{r}. Alexandre Duret-Lutz 2012-04-27 00:18:08 +02:00
  • d6587cf531 Implement dual rewritings rules for <>->. Alexandre Duret-Lutz 2012-04-26 18:12:01 +02:00
  • 6f46345c3a Implement 11 rewritings for []->. Alexandre Duret-Lutz 2012-04-26 17:13:56 +02:00
  • 6eb830c8ae Implement star-normal-form rewriting. Alexandre Duret-Lutz 2012-04-25 18:50:31 +02:00
  • e7cf7b422d Trivially reduce f;f to f[*2], f[*1..3];f to f[*2..4], etc. Alexandre Duret-Lutz 2012-04-25 15:14:14 +02:00
  • 4a775a17a3 Trivially reduce [*];f to [*] if f accepts the empty word. Alexandre Duret-Lutz 2012-04-24 18:36:20 +02:00
  • e06b3b7974 Trivially reduce 1[*]&&f = f and 1[*]|f = 1[*]. Alexandre Duret-Lutz 2012-04-24 17:22:23 +02:00
  • 5bea6e4950 Fix handling of 1 in trivial identities for rational operators. Alexandre Duret-Lutz 2012-04-19 18:09:20 +02:00
  • 691119c188 Introduce AndRat and OrRat operator. Alexandre Duret-Lutz 2012-04-18 19:20:43 +02:00
  • 35b41331f7 Add more simplification rules for AndNLM. Alexandre Duret-Lutz 2012-04-18 01:00:49 +02:00
  • f7c64060c8 Fix translation of AndNLM and Fusion operators. Alexandre Duret-Lutz 2012-04-17 19:38:09 +02:00
  • 866384b423 Fix trivial rules for b₁:b₂ and b&f. Alexandre Duret-Lutz 2012-04-17 18:33:39 +02:00
  • a4353d3985 Trivially reduce 'a[*1]' to 'a'. Alexandre Duret-Lutz 2012-04-17 16:00:22 +02:00
  • abaf102746 Get rid of bunop::Equal and bunop::Goto. Alexandre Duret-Lutz 2012-04-15 00:13:42 +02:00
  • 210723e30c Implement [->i..j] and [=i..j] as sugar with [*i..j]. Alexandre Duret-Lutz 2012-04-14 23:18:37 +02:00