Commit graph

  • 4b70453d74 * HACKING: Typo Alexandre Duret-Lutz 2013-03-28 14:14:28 +01:00
  • 6835973abe * src/tgba/tgbascc.cc: 80 columns. Alexandre Duret-Lutz 2013-03-26 10:13:30 +01:00
  • f36551d418 * NEWS, configure.ac: Bump version. Alexandre Duret-Lutz 2013-03-06 11:00:59 +01:00
  • ea911a7882 Release Spot 1.0.2. Alexandre Duret-Lutz 2013-03-06 09:21:47 +01:00
  • c6406995fb ltl_simplifier: add a boolean_to_isop option and method Alexandre Duret-Lutz 2013-03-05 23:23:45 +01:00
  • c17f3b8656 * NEWS: Document recent changes. Alexandre Duret-Lutz 2013-03-05 22:32:32 +01:00
  • 0b21af5893 cgi: fix displaying of TA and GTA Alexandre Duret-Lutz 2013-03-05 22:16:57 +01:00
  • abb5170565 cgi: Add an nondeterministic monitor option Alexandre Duret-Lutz 2013-03-05 22:02:34 +01:00
  • c892599494 Fix two memory leak reported by Sonali Dutta. Alexandre Duret-Lutz 2013-03-05 21:09:01 +01:00
  • 30e0541268 ltl2tgba: cleanup option display for monitors Alexandre Duret-Lutz 2013-03-05 21:06:36 +01:00
  • b6b6582b05 bin: Fix handling of LTL simplification options. Alexandre Duret-Lutz 2013-03-02 15:15:47 +01:00
  • 543de07737 Improve some Doxygen comments. Alexandre Duret-Lutz 2013-02-20 11:43:28 +01:00
  • 370f329671 tl: work around setup that pass -pvc automatically Alexandre Duret-Lutz 2013-02-20 10:49:59 +01:00
  • 6bd23480ab * .dir-locals.el: Remove extra parenthese. Alexandre Duret-Lutz 2013-02-12 22:51:55 +01:00
  • 9c4e9c896f Fix some VPATH related bugs. Thomas Badie 2013-01-28 22:04:19 +01:00
  • 9386923074 * NEWS, configure.ac: Bump version to 1.0.1a. Alexandre Duret-Lutz 2013-01-23 15:42:18 +01:00
  • 63fbc505f8 Release Spot 1.0.1 Alexandre Duret-Lutz 2013-01-23 14:51:57 +01:00
  • b31ddb787d * src/bin/man/Makefile.am (common_dep): Fix dependency. Alexandre Duret-Lutz 2013-01-23 14:56:44 +01:00
  • 3f61a34bd1 * src/tgbatest/ltlcross2.test: Fix list of tested configurations. Alexandre Duret-Lutz 2013-01-22 11:45:45 +01:00
  • 362c396356 * src/tgbaalgos/postproc.cc (count_states): Speed up explicit case. Alexandre Duret-Lutz 2013-01-21 18:08:51 +01:00
  • 76988369dc * src/tgbaalgos/minimize.hh: Fix documentation. Alexandre Duret-Lutz 2013-01-21 14:57:56 +01:00
  • 5e10057cfc cycles: fix documentation. Alexandre Duret-Lutz 2013-01-13 22:23:17 +01:00
  • 6a547371d7 ltlcross: diagnose missing i/o specifications earlier. Alexandre Duret-Lutz 2013-01-21 10:20:25 +01:00
  • edd687a301 ltlparse: Add compatibility with ltl2dsar's input. Alexandre Duret-Lutz 2013-01-19 15:29:27 +01:00
  • 3a5eec42de lbt: Do not write a trailing space. Alexandre Duret-Lutz 2013-01-19 15:27:57 +01:00
  • bf3c3aecde tostring: quote U, W, M, R when used as atomic propositions Alexandre Duret-Lutz 2013-01-19 14:15:17 +01:00
  • 5086e24165 ltlcross: Display the number of timeouts. Alexandre Duret-Lutz 2013-01-18 23:28:30 +01:00
  • c5461335c9 ltl2tgba on-line: display edge and transition count Alexandre Duret-Lutz 2013-01-15 19:14:22 +01:00
  • b99cfa88bb Fix two dead assignments detected by clang's static analyzer. Alexandre Duret-Lutz 2013-01-17 11:36:59 +01:00
  • dcd4644d42 eltl2tgba: slight cleanup of the tests. Alexandre Duret-Lutz 2013-01-17 11:30:16 +01:00
  • d580cce685 Fix documentation errors reported by clang++ 3.2. Alexandre Duret-Lutz 2013-01-17 09:05:25 +01:00
  • aa7b43eadf Fix several warnings reported by clang++ 3.2. Alexandre Duret-Lutz 2013-01-16 08:52:27 +01:00
  • 361f594655 Test previous patch. Alexandre Duret-Lutz 2013-01-14 18:26:04 +01:00
  • 67b7b86d52 tgbaproduct: fix segfault Pierre PARUTTO 2013-01-14 17:18:23 +01:00
  • e4ecc2d465 simplify: add four simplification rules for GF and FG Alexandre Duret-Lutz 2013-01-11 16:07:10 +01:00
  • 2580fc6f91 * src/tgbatest/babiak.test: Rewrite using ltlcross. Alexandre Duret-Lutz 2013-01-10 18:42:36 +01:00
  • 081aa0d120 tgbatest: Rewrite ltl2neverclaim using ltlcross. Alexandre Duret-Lutz 2013-01-10 18:22:35 +01:00
  • 0e74b76521 Work around Debian's patched libtool. Alexandre Duret-Lutz 2013-01-10 16:45:54 +01:00
  • c55f282298 * src/bin/common_setup.cc: Bump copyright year. Alexandre Duret-Lutz 2013-01-06 21:44:38 +01:00
  • 86558f1a5c Add missing copyright notice. Alexandre Duret-Lutz 2013-01-06 21:44:15 +01:00
  • d02376aaa2 * NEWS: Update with recent changes. Alexandre Duret-Lutz 2013-01-06 19:55:10 +01:00
  • 254896d5d8 Remove anything related to evtgba. Alexandre Duret-Lutz 2013-01-06 19:26:32 +01:00
  • 16c7bc1975 bench: delete useless defs.in files. Alexandre Duret-Lutz 2013-01-06 19:03:56 +01:00
  • 885a535184 Rewrite the ltl2tgba bench using ltlcross Alexandre Duret-Lutz 2013-01-06 18:57:50 +01:00
  • e2f17f65b8 Remove LBTT. Alexandre Duret-Lutz 2012-10-27 20:11:55 +02:00
  • a577850eb3 Address several issues reported by cppcheck all over the place. Alexandre Duret-Lutz 2012-12-20 17:18:56 +01:00
  • a3b49f1108 acccompl: Speed up. Alexandre Duret-Lutz 2012-12-20 17:16:56 +01:00
  • ce21af6323 * .dir-locals.el: Fix whitespace-mode configuration. Alexandre Duret-Lutz 2012-12-20 17:14:38 +01:00
  • 15c9b72f13 [buddy] * src/bdd.h: Make all inplace operators return a reference. Alexandre Duret-Lutz 2012-12-20 16:42:33 +01:00
  • 13c41ee773 ltlast: use the return of insert() to avoid a double lookup Alexandre Duret-Lutz 2012-12-19 17:37:13 +01:00
  • 2776de87da More documentation. Alexandre Duret-Lutz 2012-12-19 15:35:34 +01:00
  • aa2374c5a2 Cosmetics. Alexandre Duret-Lutz 2012-12-19 15:23:29 +01:00
  • cffbb7b498 Remove useless variable. Alexandre Duret-Lutz 2012-12-13 10:46:02 +01:00
  • b3d8b0198f x-to-1: Honor $PERL Alexandre Duret-Lutz 2012-12-13 10:40:22 +01:00
  • 41265cd94f * NEWS: Document recent bug fixes. Alexandre Duret-Lutz 2012-11-28 17:53:43 +01:00
  • 64484e7816 Print F"proc.st" as Fproc.st. Alexandre Duret-Lutz 2012-11-28 17:27:14 +01:00
  • af639e58c7 more files to ignore Alexandre Duret-Lutz 2012-11-28 16:45:04 +01:00
  • 5efb66cb25 Add a .dir-locals.el file. Alexandre Duret-Lutz 2012-11-27 15:19:20 +01:00
  • d10e772d35 Fix non determinism in the simulation. Thomas Badie 2012-11-13 22:10:18 +01:00
  • 49d384b1eb ltlcross: diagnose failure to write into temporary files Alexandre Duret-Lutz 2012-11-14 15:10:58 +01:00
  • 973c5bc050 * NEWS, configure.ac: Bump version to 1.0a Alexandre Duret-Lutz 2012-10-27 12:11:59 +02:00
  • 213b67e84b Release Spot 1.0. Alexandre Duret-Lutz 2012-10-27 09:30:56 +02:00
  • f9373e4a9f * m4/ax_prefix_config_h.m4: Update to more recent version. Alexandre Duret-Lutz 2012-10-26 09:47:51 +02:00
  • e2ed5f6b98 * NEWS: rephrase some items Alexandre Duret-Lutz 2012-10-26 07:56:47 +02:00
  • 301ad1ebf0 Speed-up translation of persistence formulas. Alexandre Duret-Lutz 2012-10-24 11:02:42 +02:00
  • 7c464246f2 * src/tgbaalgos/ltl2tgba_fm.cc: Typo in comment. Alexandre Duret-Lutz 2012-10-24 10:16:19 +02:00
  • d552be308b ltlcross: Add a --stop-on-error option. Alexandre Duret-Lutz 2012-10-23 23:10:07 +02:00
  • 1f12ad8765 unabbreviate_wm: fix a segfault. Alexandre Duret-Lutz 2012-10-23 22:00:17 +02:00
  • aede62d123 * src/bin/man/genltl.x: Missing dot. Alexandre Duret-Lutz 2012-10-22 20:29:14 +02:00
  • f3ef9de0be rename ltlcheck as ltlcross Alexandre Duret-Lutz 2012-10-21 13:23:02 +02:00
  • fa4e6effa6 tgbaexplicit: fix state_is_accepting() Alexandre Duret-Lutz 2012-10-20 23:58:30 +02:00
  • 76787b23c0 postproc: add the possibility to output a monitor Alexandre Duret-Lutz 2012-10-20 20:18:01 +02:00
  • 5f6c262ae5 * NEWS: Document to_wring_string(). Alexandre Duret-Lutz 2012-10-20 19:20:28 +02:00
  • 877082bfb0 Add a parse_boolean() function to use in parsers for Automata. Alexandre Duret-Lutz 2012-10-20 19:18:54 +02:00
  • da5f7ac3aa to_string: remove extra parentheses Alexandre Duret-Lutz 2012-10-20 13:52:44 +02:00
  • 0fc3c6bcff Add support for printing LTL formulas using Wring's syntax. Alexandre Duret-Lutz 2012-10-20 13:32:05 +02:00
  • bf765480b1 * src/tgba/tgbaexplicit.hh: Fix hash_map definition to please old g++. Alexandre Duret-Lutz 2012-10-20 12:18:06 +02:00
  • b8ed85a30d bin: Adjust version display and help options. Alexandre Duret-Lutz 2012-10-19 22:50:19 +02:00
  • c6030df936 accconv: speed up acceptance_convertor::as_positive_product() Alexandre Duret-Lutz 2012-10-19 20:50:35 +02:00
  • 31fb3d9d15 tgbaexplicit: speed up merge_transitions() Alexandre Duret-Lutz 2012-10-19 17:53:08 +02:00
  • 0bdfd9c72c * src/bin/ltlcheck.cc: Cleanup temporary files on ^C. Alexandre Duret-Lutz 2012-10-19 16:17:53 +02:00
  • e426c63550 lbttparse: allow acceptance sets that are not consecutive integers. Alexandre Duret-Lutz 2012-10-19 15:56:42 +02:00
  • 89b9cc5fd5 lbttparse: make sure we parse wring2lbtt's output Alexandre Duret-Lutz 2012-10-18 13:58:38 +02:00
  • 676ab41f6f ltlparse: diagnose empty (...) block in lenient mode. Alexandre Duret-Lutz 2012-10-18 00:23:34 +02:00
  • ff0eada81d * NEWS: Mention lenient parsing. Alexandre Duret-Lutz 2012-10-17 18:46:04 +02:00
  • 86dac4aadf ltlparse: add a lenient parsing mode Alexandre Duret-Lutz 2012-10-16 19:29:40 +02:00
  • d9ceb4adc4 bin: plug several memory leaks Alexandre Duret-Lutz 2012-10-15 20:54:28 +02:00
  • 9f1d369563 * src/bin/ltlcheck.cc: Add a --no-checks option. Alexandre Duret-Lutz 2012-10-15 20:41:44 +02:00
  • 2977635ae5 ltlcheck: do not check duplicate formulas Alexandre Duret-Lutz 2012-10-15 18:21:38 +02:00
  • 35fc975d1e * NEWS: mention ltlcheck Alexandre Duret-Lutz 2012-10-15 17:48:01 +02:00
  • f03ba4b56f man page cosmetics Alexandre Duret-Lutz 2012-10-15 17:37:47 +02:00
  • b2a5d5aa62 ltlcheck: add options --json and --csv Alexandre Duret-Lutz 2012-10-15 17:31:43 +02:00
  • fc374c0790 * src/tgbatest/spotlbtt.test: Remove superfluous options. Alexandre Duret-Lutz 2012-10-15 15:14:51 +02:00
  • 2fe8f025e3 ltlcheck: add a "Sanity check..." message Alexandre Duret-Lutz 2012-10-14 19:08:03 +02:00
  • 7d6fc328ab Add new tests for LTL and PSL translation, based on ltlcheck. Alexandre Duret-Lutz 2012-10-14 19:06:59 +02:00
  • d1871d87dc * src/bin/ltlcheck.cc: Diagnose missing output format. Alexandre Duret-Lutz 2012-10-14 18:29:34 +02:00
  • 8e9002947e ltlcheck: do not ignore ^C during sanity checks Alexandre Duret-Lutz 2012-10-14 18:27:50 +02:00
  • 7022853dad * src/ltlvisit/simplify.cc (simplify_visitor): Return automatop as-is. Alexandre Duret-Lutz 2012-10-14 18:25:36 +02:00
  • 7b6337f456 ltlcheck: Add a man page. Alexandre Duret-Lutz 2012-10-14 17:37:26 +02:00
  • b2de0136b2 Add a has_lbt_atomic_props() method to LTL formulas. Alexandre Duret-Lutz 2012-10-14 15:52:53 +02:00