Commit graph

  • d7b3d05e57 minato: use bdd_ite() Alexandre Duret-Lutz 2020-06-09 20:23:42 +02:00
  • af108d0556 * doc/org/ioltl.org: Document prefix operators. Alexandre Duret-Lutz 2020-07-31 12:05:32 +02:00
  • fd437d62f8 help2man: allow line breaks in long lists of options Alexandre Duret-Lutz 2020-07-29 21:28:01 +02:00
  • ceced82c5c * debian/rules (fix-js): Adjust to newer MathJax URL. Alexandre Duret-Lutz 2020-07-29 15:17:47 +02:00
  • fde9a303c4 to_parity: minor fixes Alexandre Duret-Lutz 2020-07-29 14:43:55 +02:00
  • 9e6a99dcac * spot/misc/satsolver.hh: Typo in comment. Alexandre Duret-Lutz 2020-07-28 22:08:47 +02:00
  • d308728b41 argp: fix handling of very long options in --help Alexandre Duret-Lutz 2020-07-28 10:30:45 +02:00
  • c49506eea7 * debian/copyright: Replace MIT by Expat. Alexandre Duret-Lutz 2020-07-27 21:47:28 +02:00
  • b013077af3 doc: improve css Alexandre Duret-Lutz 2020-07-27 17:05:58 +02:00
  • 1a7f471a02 * tests/python/ipnbdoctest.py: Ignore matplotlib font cache messages. Alexandre Duret-Lutz 2020-07-27 10:26:17 +02:00
  • 94eca2ca7d * spot/twaalgos/toparity.hh: Improve documentation. Alexandre Duret-Lutz 2020-07-24 15:39:24 +02:00
  • 50a33cbc8c org: fix shadow of hierarchy figure Alexandre Duret-Lutz 2020-07-23 15:46:21 +02:00
  • 2c267cac40 simplify: fix handling of keep_top_xor Alexandre Duret-Lutz 2020-07-22 16:23:34 +02:00
  • f179c79409 * doc/org/ioltl.org: Document prefix operators. Alexandre Duret-Lutz 2020-07-31 12:05:32 +02:00
  • 672e6248b8 help2man: allow line breaks in long lists of options Alexandre Duret-Lutz 2020-07-29 21:28:01 +02:00
  • a8db30d676 * debian/rules (fix-js): Adjust to newer MathJax URL. Alexandre Duret-Lutz 2020-07-29 15:17:47 +02:00
  • 3710e8f283 to_parity: minor fixes Alexandre Duret-Lutz 2020-07-29 14:43:55 +02:00
  • a375089e52 simplify_acceptance: generalize the complementary mark rewriting Alexandre Duret-Lutz 2020-07-29 14:37:38 +02:00
  • 0c4b701630 improve acceptance simplifications using useless colors Alexandre Duret-Lutz 2020-07-28 22:09:33 +02:00
  • c341a3cabf * spot/misc/satsolver.hh: Typo in comment. Alexandre Duret-Lutz 2020-07-28 22:08:47 +02:00
  • 25cb7651fe cleanacc: merge algorithms dealing with included and identical sets Alexandre Duret-Lutz 2020-07-28 15:35:57 +02:00
  • a804f964d2 argp: fix handling of very long options in --help Alexandre Duret-Lutz 2020-07-28 10:30:45 +02:00
  • 31fd31436a * debian/copyright: Fix bricks' license, and replace MIT by Expat. Alexandre Duret-Lutz 2020-07-27 21:47:28 +02:00
  • cba762a60f doc: improve css Alexandre Duret-Lutz 2020-07-27 17:05:58 +02:00
  • 3220da6605 tra_to_tba: finish 05e6e0885 Alexandre Duret-Lutz 2020-07-27 11:08:51 +02:00
  • ff3a3f8144 * tests/python/ipnbdoctest.py: Ignore matplotlib font cache messages. Alexandre Duret-Lutz 2020-07-27 10:26:17 +02:00
  • 5ec9d55fea simplify_acceptance: Use color inclusions to simplify a condition Florian Renkin 2020-07-25 19:15:17 +02:00
  • 05e6e08859 tra_to_tba: remove more useless edges Alexandre Duret-Lutz 2020-07-24 16:24:28 +02:00
  • 567a5439c5 * spot/twaalgos/toparity.hh: Improve documentation. Alexandre Duret-Lutz 2020-07-24 15:39:24 +02:00
  • 7fbf4e0e3c remove_fin: ignore more useless transitions Alexandre Duret-Lutz 2020-07-24 15:38:42 +02:00
  • 91db0e1e29 org: fix shadow of hierarchy figure Alexandre Duret-Lutz 2020-07-23 15:46:21 +02:00
  • b17376879d translate: add a quick syntactic simplification before relabeling Alexandre Duret-Lutz 2020-07-22 16:31:53 +02:00
  • 1c5468a93a simplify: fix handling of keep_top_xor Alexandre Duret-Lutz 2020-07-22 16:23:34 +02:00
  • 1784671ca1 Merge branch 'master' into next Alexandre Duret-Lutz 2020-07-22 08:13:26 +02:00
  • 2ce84f7889 * configure.ac, NEWS: Bump version to 2.9.3.dev. Alexandre Duret-Lutz 2020-07-22 08:12:01 +02:00
  • 0b6a7998af Release Spot 2.9.3 Alexandre Duret-Lutz 2020-07-22 08:09:56 +02:00
  • cc498e7080 org: run a spell checker on the documentation Alexandre Duret-Lutz 2020-07-21 22:15:54 +02:00
  • 0342161b20 org: fix python execution with in-tree source and Swig4 Alexandre Duret-Lutz 2020-07-21 21:21:50 +02:00
  • d5f488647b ltlcross: completely fix #420 Alexandre Duret-Lutz 2020-07-21 16:08:03 +02:00
  • f3b8bf8e56 org: run a spell checker on the documentation Alexandre Duret-Lutz 2020-07-21 22:15:54 +02:00
  • 0fbc83e9c2 org: fix python execution with in-tree source and Swig4 Alexandre Duret-Lutz 2020-07-21 21:21:50 +02:00
  • 457e130e24 ltlcross: completely fix #420 Alexandre Duret-Lutz 2020-07-21 16:08:03 +02:00
  • 1a0c8a44ba Merge branch 'master' into next Alexandre Duret-Lutz 2020-07-21 08:28:13 +02:00
  • d61d6570ac * NEWS, configure.ac: Bump version to 2.9.2.dev. Alexandre Duret-Lutz 2020-07-21 08:24:52 +02:00
  • 66a6fbdcb1 Release Spot 2.9.2 Alexandre Duret-Lutz 2020-07-21 08:22:06 +02:00
  • ac5a261aa5 ltlcross: fix cross-checks for automata using Fin acceptance Alexandre Duret-Lutz 2020-07-20 12:10:20 +02:00
  • c7774ebb55 C++20: fix warnings reported by g++ 10.1 Alexandre Duret-Lutz 2020-07-16 16:45:28 +02:00
  • df39000d8e * doc/org/setup.org: Fix release date. Alexandre Duret-Lutz 2020-07-16 10:31:00 +02:00
  • 33b28c8151 ltlcross: fix cross-checks for automata using Fin acceptance Alexandre Duret-Lutz 2020-07-20 12:10:20 +02:00
  • 4db6a342da Fixes #419 Etienne Renault 2020-07-17 08:21:23 +02:00
  • 9daa4e60a4 formula: make operator bool explicit Alexandre Duret-Lutz 2020-07-17 11:39:55 +02:00
  • a8959ecf81 C++20: work around g++ 10.1 bug #95242 Alexandre Duret-Lutz 2020-07-16 21:56:17 +02:00
  • 368acaad28 C++20: fix warnings reported by g++ 10.1 Alexandre Duret-Lutz 2020-07-16 16:45:28 +02:00
  • a7ff5b4eed [buddy] build in C++17 mode by default Alexandre Duret-Lutz 2020-07-16 12:14:04 +02:00
  • 4f23097619 build in C++17 mode by default Alexandre Duret-Lutz 2020-07-16 12:12:21 +02:00
  • a770727ee8 * doc/org/setup.org: Fix release date. Alexandre Duret-Lutz 2020-07-16 10:31:00 +02:00
  • 1513a9d996 Merge branch 'master' into next Alexandre Duret-Lutz 2020-07-15 14:06:23 +02:00
  • cf1550c352 * NEWS, configure.ac: Bump version to 2.9.1.dev. Alexandre Duret-Lutz 2020-07-15 13:43:15 +02:00
  • 6205664297 Release Spot 2.9.1 Alexandre Duret-Lutz 2020-07-15 13:40:59 +02:00
  • 94c189b29d remfin: simplify, thanks to previous patch Alexandre Duret-Lutz 2020-07-15 11:41:14 +02:00
  • b214fd75d6 scc_info: honor filters in edges_of() and inner_edges_of() Alexandre Duret-Lutz 2020-07-15 11:30:52 +02:00
  • 1fa048fe8a ltlcross: diagnose complementations requiring too many colors Alexandre Duret-Lutz 2020-07-13 17:59:55 +02:00
  • f2403c91dc run: fix reduce on automata with Fin Alexandre Duret-Lutz 2020-07-10 18:05:18 +02:00
  • 9caba8bfe8 genem: replace one recursive call by a loop Alexandre Duret-Lutz 2020-06-18 15:32:54 +02:00
  • a3769dfd81 address a new g++-10 warnings Alexandre Duret-Lutz 2020-06-09 00:32:48 +02:00
  • e20bae6609 swig: search for swig4.0 Alexandre Duret-Lutz 2020-06-09 00:14:36 +02:00
  • 4cfa253830 ltldo: improve error messages Alexandre Duret-Lutz 2020-05-31 16:19:51 +02:00
  • 3368b4b99f * tests/sanity/80columns.test: Force LC_ALL. Alexandre Duret-Lutz 2020-05-30 14:28:50 +02:00
  • f16bc8a58b sccinfo: fix doc Alexandre Duret-Lutz 2020-05-29 17:14:17 +02:00
  • 9e075e7312 twa: get rid of set_num_sets_() Alexandre Duret-Lutz 2020-05-25 10:51:44 +02:00
  • 37d0b0d045 ltlsynt: use wdba-minimize=2 and ba-simul=0 Alexandre Duret-Lutz 2020-05-24 20:32:27 +02:00
  • 56c8d690ba ltlsynt: Change default options Florian Renkin 2020-05-23 14:31:59 +02:00
  • 8ac24acbf8 ltlsynt: Add more elements in csv Florian Renkin 2020-05-23 14:29:48 +02:00
  • 7c09f64c49 ltlsynt: Add -x option for translation Florian Renkin 2020-05-23 14:13:33 +02:00
  • e06f8a3ece work around diagnostic changes in Bison 3.6 Alexandre Duret-Lutz 2020-05-24 14:05:46 +02:00
  • 16540869d4 ltlsynt: add --algo=ps Alexandre Duret-Lutz 2020-05-24 09:45:35 +02:00
  • b434ac7f8a simplify_acc: perform unit-propagation earlier Alexandre Duret-Lutz 2020-05-23 12:00:56 +02:00
  • b762f54228 remfin: do not clone transitions that are accepting in main Alexandre Duret-Lutz 2020-05-23 11:56:16 +02:00
  • c005041e53 improve fuse_marks_here by detecting more patterns Alexandre Duret-Lutz 2020-05-22 16:09:26 +02:00
  • ce695e67f9 fixpool: allocate a new chunk on creation Alexandre Duret-Lutz 2020-05-22 15:33:40 +02:00
  • 64aee87d76 postproc: option to wdba-minimize only when sure Alexandre Duret-Lutz 2020-05-21 15:42:05 +02:00
  • 8744751ec0 * doc/org/satmin.org: Remove extra newlines (fixes #410). Alexandre Duret-Lutz 2020-05-18 17:08:40 +02:00
  • d25fcb23eb stats: speed up the computation of transitions Alexandre Duret-Lutz 2020-05-18 16:52:31 +02:00
  • 4608d9a5b1 [buddy] avoid cache errors in bdd_satcount() and friends Alexandre Duret-Lutz 2020-05-18 19:25:14 +02:00
  • fc1c17b91c ltlsynt: make sure the previous Xor optimization actually works Alexandre Duret-Lutz 2020-05-16 19:22:28 +02:00
  • 6ec6150462 translate: improve handling of Xor and Equiv at top-level for -G -D Alexandre Duret-Lutz 2020-05-16 18:03:38 +02:00
  • 822b749166 product: add product_xor() and product_xnor() Alexandre Duret-Lutz 2020-05-16 16:20:39 +02:00
  • 918548a03d run: fix reduce on automata with Fin Alexandre Duret-Lutz 2020-07-10 18:05:18 +02:00
  • 6dbdd89fc1 genem: replace one recursive call by a loop Alexandre Duret-Lutz 2020-06-18 15:32:54 +02:00
  • b3c7994a1d bricks: rework tests Etienne Renault 2020-06-10 14:46:35 +02:00
  • f748281719 HACKING: precisions for debugging under MacOS Etienne Renault 2020-06-10 11:49:47 +02:00
  • 68014e46fc HACKING: rename src to spot Etienne Renault 2020-06-09 20:39:56 +02:00
  • 9b4d51e3db cube: prefer value_initialization Etienne Renault 2020-06-09 16:29:51 +02:00
  • 9411dab738 lpar13: avoid leak when counterexample detected Etienne Renault 2020-06-09 17:04:26 +02:00
  • 13402a63c4 bloemen_ec: avoid leak when counterexample detected Etienne Renault 2020-06-09 16:36:32 +02:00
  • 6a12b77360 sanity: fixes #417 Etienne Renault 2020-06-09 13:06:12 +02:00
  • 47b31bd9eb bricks: include tests in test-suite Etienne Renault 2020-06-09 12:58:27 +02:00
  • 2098d41c05 bricks: details version and modifications Etienne Renault 2020-06-09 09:35:44 +02:00
  • 7d69708f73 modelchek: add more tests Etienne Renault 2020-06-09 09:16:06 +02:00
  • c94d877c98 modelcheck: adjust default value for deadlock Etienne Renault 2020-06-09 09:15:07 +02:00