Commit graph

  • 1a36ea6ce4 ltlsynt: fix usage for --dot's argument Alexandre Duret-Lutz 2024-09-02 17:26:42 +02:00
  • 514209e80f * configure.ac: Typo. Alexandre Duret-Lutz 2024-09-02 13:54:36 +02:00
  • f5ab5678b5 python: improve support of spot-extra, and recent swig Alexandre Duret-Lutz 2024-09-02 13:50:36 +02:00
  • cc0f6f1e0d game: fix solving "parity min" games with multi-colored edges Alexandre Duret-Lutz 2024-08-30 16:05:50 +02:00
  • 97832af321 randltl: fix generation without unary operators Alexandre Duret-Lutz 2024-08-21 21:36:54 +02:00
  • bdc63db9f0 ltlgrind: improve error message when formulas are missing Alexandre Duret-Lutz 2024-08-21 11:18:14 +02:00
  • 783efa2fe8 * doc/tl/tl.tex: Some typos. Alexandre Duret-Lutz 2024-07-25 18:01:42 +02:00
  • e48506f548 improve some comments Alexandre Duret-Lutz 2024-07-04 12:11:10 +02:00
  • e13deeb143 * .gitlab-ci.yml (publish-stable): Add scp for LRE's dload host. Alexandre Duret-Lutz 2024-09-23 11:49:26 +02:00
  • b9cb4022cf gen: rename pps-arbiter's APs Alexandre Duret-Lutz 2024-09-19 11:40:53 +02:00
  • 40a45eff22 * doc/org/ltlmix.org: Typos. Alexandre Duret-Lutz 2024-09-19 08:50:41 +02:00
  • 7b0e15a7fb implement maximum cardinality search Alexandre Duret-Lutz 2024-09-18 12:04:23 +02:00
  • 77a17881a3 defrag_states: allow a permutation of state numbers Alexandre Duret-Lutz 2024-09-17 17:10:27 +02:00
  • 4ccdcb4a5b tests: rewrite the syntimpl test Alexandre Duret-Lutz 2024-09-12 17:28:17 +02:00
  • 99a622059c synthesis: fix handling of deadstates Alexandre Duret-Lutz 2024-09-12 14:00:08 +02:00
  • 90fb7b1cd9 * doc/org/ltlmix.org: Fix example. Alexandre Duret-Lutz 2024-09-11 11:38:12 +02:00
  • 1724d2b14c ltlsynt: -q should also hide status and AIG output Alexandre Duret-Lutz 2024-09-09 17:02:49 +02:00
  • 950b205b63 ltlsynt: have --csv exclude the formula column by default Alexandre Duret-Lutz 2024-09-09 16:45:00 +02:00
  • 5488cb75c6 ltlsynt: overhaul CSV output Alexandre Duret-Lutz 2024-09-09 16:28:51 +02:00
  • b729aa3f30 ltlsynt: fix a few issues with --csv Alexandre Duret-Lutz 2024-09-04 22:47:50 +02:00
  • a22a05b8ec ltlsynt: implement --csv-without-formula Alexandre Duret-Lutz 2024-09-04 16:33:48 +02:00
  • 6e5592fe6a ltlsynt: save source filename with --csv Alexandre Duret-Lutz 2024-09-04 16:17:46 +02:00
  • 45cb9caa0e game: avoid a spurious g++14 warning Alexandre Duret-Lutz 2024-09-03 17:37:59 +02:00
  • e6ebbdf65f ltlfilt, ltlsynt, ltlmix: add a --part-file option Alexandre Duret-Lutz 2024-09-03 14:20:17 +02:00
  • 388d005635 fix spurious g++-14 warning Alexandre Duret-Lutz 2024-09-02 17:28:28 +02:00
  • a8a0a1973e ltlsynt: fix usage for --dot's argument Alexandre Duret-Lutz 2024-09-02 17:26:42 +02:00
  • 8eec295e23 * configure.ac: Typo. Alexandre Duret-Lutz 2024-09-02 13:54:36 +02:00
  • c9911962d4 python: improve support of spot-extra, and recent swig Alexandre Duret-Lutz 2024-09-02 13:50:36 +02:00
  • 89a06772b8 game: fix solving "parity min" games with multi-colored edges Alexandre Duret-Lutz 2024-08-30 16:05:50 +02:00
  • c5d991e55c autfilt: add a --track-formula option Alexandre Duret-Lutz 2024-08-30 11:38:26 +02:00
  • 3d3e87948c twaalgos: add a match_states variant with a formula argument Alexandre Duret-Lutz 2024-08-29 11:16:35 +02:00
  • 5f1d00b858 twaalgos: introduce match_states(a,b) Alexandre Duret-Lutz 2024-08-28 15:57:33 +02:00
  • b549e8e8c1 * doc/org/ltlmix.org: Fix several typos. Alexandre Duret-Lutz 2024-08-27 00:28:35 +02:00
  • 3e90265ce7 org: add example of ltlmix used on synthesis specifications Alexandre Duret-Lutz 2024-08-26 16:08:05 +02:00
  • c6f4b18655 genltl: add --lily-patterns Alexandre Duret-Lutz 2024-08-26 15:27:23 +02:00
  • 844fb887d9 ltlmix: add support for the I/O variants Alexandre Duret-Lutz 2024-08-26 11:42:09 +02:00
  • 6fa42c90b8 ltlfilt: add support for --relabel=io, --ins, and --outs Alexandre Duret-Lutz 2024-08-23 17:22:17 +02:00
  • bea1713f4e ltlsynt: extract In/Out AP processing in separate file Alexandre Duret-Lutz 2024-08-23 16:05:14 +02:00
  • 2390a89986 ltlmix: learn option -R for random conjuncts Alexandre Duret-Lutz 2024-08-23 15:17:04 +02:00
  • c8b8ac60be bin: new ltlmix tool Alexandre Duret-Lutz 2024-08-22 17:04:48 +02:00
  • baf2778c9a randltl: fix generation without unary operators Alexandre Duret-Lutz 2024-08-21 21:36:54 +02:00
  • 436e5a2d7f ltlgrind: improve error message when formulas are missing Alexandre Duret-Lutz 2024-08-21 11:18:14 +02:00
  • 3693bbab08 synthesis: rewrite a C++20 construct into C++17 Alexandre Duret-Lutz 2024-08-20 16:52:27 +02:00
  • a0a6ec6794 * doc/tl/tl.tex: Some typos. Alexandre Duret-Lutz 2024-07-25 18:01:42 +02:00
  • 44efc96595 formula: add a missing trivial rewriting in SERE Alexandre Duret-Lutz 2024-07-25 17:56:04 +02:00
  • bcdfe44c44 ltlfilt: add support for --to-delta2 Alexandre Duret-Lutz 2024-07-25 16:34:11 +02:00
  • 41abe3f831 tl: implement to_delta2() Alexandre Duret-Lutz 2024-07-25 10:42:58 +02:00
  • 5bc4d12bba ltlfilt: support --pi1 --sigma1 --delta1 --pi2 --sigma2 Alexandre Duret-Lutz 2024-07-19 18:18:12 +02:00
  • 7901a37747 formula: track Δ₁, Σ₂, Π₂, and Δ₂ membership Alexandre Duret-Lutz 2024-07-19 17:04:21 +02:00
  • 0c52c49079 doc: fix documentation of P and R classes Alexandre Duret-Lutz 2024-07-18 16:36:01 +02:00
  • 6a7ef4db3f postprocess: call restrict_dead_end_edges_here() Alexandre Duret-Lutz 2024-07-17 16:59:07 +02:00
  • 31511e042a twaalgos: implement restrict_dead_end_edges_here() Alexandre Duret-Lutz 2024-07-15 15:27:57 +02:00
  • f03e32619a improve some comments Alexandre Duret-Lutz 2024-07-04 12:11:10 +02:00
  • 5ddac258e1 Introduce new ways to split an automaton Philipp Schlehuber 2024-03-03 22:15:27 +01:00
  • 2274308cad reduce_mealy_here: do not reduce when size is 1 Florian Renkin 2024-05-17 13:13:59 +00:00
  • c7c18db6db work around GCC bug 108860 Alexandre Duret-Lutz 2024-06-27 15:39:15 +02:00
  • fdb09f787e * spot.spec.in: Update URL and description. Alexandre Duret-Lutz 2024-05-20 16:15:57 +02:00
  • 6420bde5fd debian: drop ipython3-notebook dependency Alexandre Duret-Lutz 2024-05-20 16:11:18 +02:00
  • 799db05111 * doc/org/tut25.org: Fix typos in the example. Alexandre Duret-Lutz 2024-05-16 22:40:52 +02:00
  • c44e03c791 * NEWS, configure.ac: Bump version to 2.12.0.dev. Alexandre Duret-Lutz 2024-05-14 15:21:02 +02:00
  • 532b57d0df Release spot 2.12 Alexandre Duret-Lutz 2024-05-14 15:19:37 +02:00
  • 913e807d66 stats: fix rounding issues Alexandre Duret-Lutz 2024-05-16 12:17:17 +02:00
  • 2bd2abd4c9 pdegen & toparity: minor refactor Alexandre Duret-Lutz 2024-05-14 10:20:45 +02:00
  • ed91f59bbd tl: new PSL trivial simplifications Alexandre Duret-Lutz 2024-05-13 22:15:15 +02:00
  • a826a4ae6f * tests/python/formulas.ipynb: Improve SONF example (fixes #578). Alexandre Duret-Lutz 2024-05-06 17:25:45 +02:00
  • c5c3e905ae python: workaround different help() output in Python 3.12 Alexandre Duret-Lutz 2024-05-03 16:32:16 +02:00
  • e6362b785b python: use raw strings when appropriate Alexandre Duret-Lutz 2024-05-03 00:05:33 +02:00
  • dbe31c72c8 Upgrade detection of Python include path for Python 3.12 Alexandre Duret-Lutz 2024-05-02 21:35:21 +02:00
  • be102e09d4 implement BA acceptance set reduction and enlargement Alexandre Duret-Lutz 2024-04-25 17:59:10 +02:00
  • ab7f4f51c4 simulation: fix determinism check Alexandre Duret-Lutz 2024-04-24 23:45:47 +02:00
  • ffddbd84d0 * NEWS: Fix some typos. Alexandre Duret-Lutz 2024-04-19 10:20:49 +02:00
  • c5490428be * tests/sanity/style.test: Fix spurious failure. Alexandre Duret-Lutz 2024-04-19 09:43:50 +02:00
  • 2ffdd84942 Rename split_independant_formulas Florian Renkin 2024-04-16 16:42:27 +02:00
  • f57782686d Rename minimize_obligation_garanteed_to_work Florian Renkin 2024-04-16 16:37:00 +02:00
  • 96ff2225e3 Fix typos in doc, comments and messages Florian Renkin 2024-04-16 16:24:54 +02:00
  • 952e502480 * .gitlab-ci.yml: Use CI_JOB_ID instead of CI_PIPELINE_ID. Alexandre Duret-Lutz 2024-04-10 21:58:47 +02:00
  • 1a5b4f00f5 * spot/twaalgos/split.hh: Typo in comment. Alexandre Duret-Lutz 2024-04-10 21:58:32 +02:00
  • 9230614f8d ltlsynt implement polarity and gequiv after decomposition too Alexandre Duret-Lutz 2024-04-05 12:42:43 +02:00
  • 848d1a3901 man: fix several issues Alexandre Duret-Lutz 2024-04-03 23:05:12 +02:00
  • a17d8a0501 help2man: work around some utf8 issues Alexandre Duret-Lutz 2024-04-03 17:47:18 +02:00
  • 27a0137208 Small fixes in the man pages pierreganty 2024-03-27 10:27:04 +01:00
  • 79b7cfea01 ltl2tgba_fm: simplify the ratexp_to_dfa interface Alexandre Duret-Lutz 2024-04-03 15:27:21 +02:00
  • 7ac570fa3f modernize some Python code Alexandre Duret-Lutz 2024-03-26 20:35:10 +01:00
  • df44f7a5c2 require python 3.6 Alexandre Duret-Lutz 2024-03-26 16:21:44 +01:00
  • 88f8af22c3 autfilt: add option --separate-edges Alexandre Duret-Lutz 2024-03-25 17:12:05 +01:00
  • 89f87795ca * doc/org/tut25.org: Minor corrections. pierreganty 2024-03-25 13:02:59 +01:00
  • 26ef5458eb determinize: speedup on automata with many AP and few labels Alexandre Duret-Lutz 2024-03-25 10:36:34 +01:00
  • bda40a5f19 simulation: heuristically use a separated-label approach to rebuild Alexandre Duret-Lutz 2024-03-22 23:01:50 +01:00
  • 7ee2d9995f genaut: add two families of cyclic automata Alexandre Duret-Lutz 2024-03-24 20:59:52 +01:00
  • 26a62c8b68 minimize: t acceptance is compatible with wdba-minimization Alexandre Duret-Lutz 2024-03-22 16:08:32 +01:00
  • 7e228e86ee hoa: add option 'b' to build an alias-based basis for all labels Alexandre Duret-Lutz 2024-03-22 14:41:42 +01:00
  • 03a4f01184 acc: work around a Swig 4.2.1 bug Alexandre Duret-Lutz 2024-03-21 22:18:15 +01:00
  • cb15840c56 org: add an example of conversion to BA format Alexandre Duret-Lutz 2024-03-19 21:21:22 +01:00
  • 06099f649e powerset: improve tgba_powerset on small automata with large |AP| Alexandre Duret-Lutz 2024-03-18 23:20:06 +01:00
  • c220107eb4 remove_alternation: use edge_separator Alexandre Duret-Lutz 2024-03-18 21:19:38 +01:00
  • 3bcffa2fcd split: add separate_edges() and a edge_separator class Alexandre Duret-Lutz 2024-03-18 16:31:07 +01:00
  • 0a045e5f76 split: factor the code common to both split_edges() versions Alexandre Duret-Lutz 2024-03-18 11:01:24 +01:00
  • ef10be047c fix previous two patches Alexandre Duret-Lutz 2024-03-18 10:37:21 +01:00
  • f26f3243dd alternation: speed up remove_alternation when few labels are used Alexandre Duret-Lutz 2024-03-17 22:42:18 +01:00
  • 1e512d422b dualize: improve performance on small automata with large |AP| Alexandre Duret-Lutz 2024-03-17 21:27:04 +01:00