Commit graph

949 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b487ff4190 Merge branch 'master' into next 2023-04-20 09:50:23 +02:00
Alexandre Duret-Lutz
b6c076ce19 release Spot 2.11.5
* NEWS, configure.ac, doc/org/setup.org: Update version.
2023-04-20 09:45:41 +02:00
Alexandre Duret-Lutz
184aa9931e org: replace version references with org-babel blocks
This way we have fewer lines to edit multiple when making releases.

* doc/org/index.org, doc/org/init.el.in, doc/org/install.org,
doc/org/setup.org, doc/org/tools.org: Use org-babel instead of macros
for release version and links.
2023-04-19 09:07:02 +02:00
Alexandre Duret-Lutz
1a0b1f235d * doc/tl/tl.tex: Typo in firstmatch semantics. 2023-04-19 09:04:16 +02:00
Alexandre Duret-Lutz
dcd4759896 org: fix rendering of R examples for recent ESS/Org
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Newer ESS version
need to be taught to use default-directory instead of the project
directory.
* doc/org/ltlcross.org: Use "result file" to render the output.
2023-04-19 09:04:07 +02:00
Alexandre Duret-Lutz
a146457ea1 * doc/org/tut03.org: Typos. 2023-04-19 09:04:02 +02:00
Alexandre Duret-Lutz
d3013b072d org: do not require org-install
org-install has been obsolete for a long time, and has been removed
from Org 9.6.

* doc/org/init.el.in: Remove org-install.
2023-04-19 09:03:53 +02:00
Alexandre Duret-Lutz
c12b0622b4 org: replace version references with org-babel blocks
This way we have fewer lines to edit multiple when making releases.

* doc/org/index.org, doc/org/init.el.in, doc/org/install.org,
doc/org/setup.org, doc/org/tools.org: Use org-babel instead of macros
for release version and links.
2023-04-18 22:18:16 +02:00
Alexandre Duret-Lutz
7a97a6080c * doc/tl/tl.tex: Typo in firstmatch semantics. 2023-03-29 16:16:06 +02:00
Alexandre Duret-Lutz
146942953a org: fix rendering of R examples for recent ESS/Org
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Newer ESS version
need to be taught to use default-directory instead of the project
directory.
* doc/org/ltlcross.org: Use "result file" to render the output.
2023-03-03 15:36:31 +01:00
Alexandre Duret-Lutz
f117159ec4 * doc/org/tut03.org: Typos. 2023-02-24 11:26:12 +01:00
Alexandre Duret-Lutz
4bd023e515 org: do not require org-install
org-install has been obsolete for a long time, and has been removed
from Org 9.6.

* doc/org/init.el.in: Remove org-install.
2023-02-16 17:46:51 +01:00
Alexandre Duret-Lutz
e16d82d5bd Merge branch 'master' into next 2023-02-10 08:53:17 +01:00
Alexandre Duret-Lutz
50a58254a7 Release spot 2.11.4
* NEWS, configure.ac, doc/org/setup.org: Update version.
2023-02-10 08:49:26 +01:00
Alexandre Duret-Lutz
403e55d555 * doc/org/spot.css: Do not define background twice. 2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
16ad7bdf77 * doc/org/spot.css: Do not define background twice. 2023-01-05 17:47:46 +01:00
Alexandre Duret-Lutz
396009c014 parseaut: better merge of multiple initial states
If an initial states without incoming transition has to be merged into
another one, its outgoing edges can be reused by just changing their
source.

* spot/parseaut/parseaut.yy (fix_initial_state): Implement this here.
* tests/core/522.test: Add more tests.
* tests/core/readsave.test: Adjust one expected output.
* doc/org/hoa.org: Mention the completeness change.
* NEWS: Mention the new feature.
2023-01-05 16:15:08 +01:00
Alexandre Duret-Lutz
b02d8328ee Merge branch 'master' into next 2022-12-09 09:45:01 +01:00
Alexandre Duret-Lutz
d7feeca13e Release Spot 2.11.3
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.3.
2022-12-09 09:40:27 +01:00
Alexandre Duret-Lutz
720c380412 formula: new trivial simplifications
Add the following rules:
  - f|[+] = [+] if f rejects [*0]
  - f|[*] = [*] if f accepts [*0]
  - f&&[+] = f if f rejects [*0]
  - b:b[*i..j] = b[*max(i,1)..j]
  - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1,1), j+l-1]

* spot/tl/formula.cc: Implement the new rules.
* doc/tl/tl.tex: Document them.
* tests/core/equals.test: Test them.
* NEWS: Add them
2022-12-09 09:30:10 +01:00
Alexandre Duret-Lutz
4629d074ab Fix semantics of [*i..j] and [:*i..j]
* doc/tl/tl.tex: After a discussion with Antoin, it appears that the
semantics previously given for f[*0..j] was not considering that f[*0]
should accept any sequence of one letter.
2022-12-07 11:26:51 +01:00
Alexandre Duret-Lutz
843c4cdb91 translate, simplify: limit containment checks of n-ary operators
Fixes #521.

* spot/tl/simplify.cc, spot/tl/simplify.hh,
spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add an option
to limit automata-based implication checks of n-ary operators when too
many operands are used.  Defaults to 16.
* bin/spot-x.cc, NEWS, doc/tl/tl.tex: Document it.
* tests/core/bdd.test: Disable the limit for this test.
2022-11-15 17:49:21 +01:00
Alexandre Duret-Lutz
66aaa11580 Release Spot 2.11.2
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.2.
2022-10-26 11:15:39 +02:00
Alexandre Duret-Lutz
c312a05bbd do not use id for animating the logo
because we remove ids using svgo...

* doc/org/spot2.svg, doc/org/spot.css: Animate the verison using a
class.
2022-10-26 10:04:48 +02:00
Alexandre Duret-Lutz
de29ba9e4c stats: add options to count unreachable states and transitions
Based on a request from Pierre Ganty.

* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: Implement those
options.
* tests/core/format.test: Add test case.
* doc/org/autfilt.org: Update doc.
* NEWS: Mention them.
2022-10-19 17:10:37 +02:00
Alexandre Duret-Lutz
666d78d499 * doc/org/init.el.in: Typo in comment. 2022-10-13 11:22:14 +02:00
Alexandre Duret-Lutz
dae46567e7 org: work around newer org-mode not displaying SVG as <object>
* doc/org/init.el.in (spot-svg-output-as-object): New function.
2022-10-11 14:54:24 +02:00
Alexandre Duret-Lutz
c2bbb3fd00 Release Spot 2.11.1
* NEWS, configure.ac, doc/org/setup.org: Update.
2022-10-10 14:13:42 +02:00
Alexandre Duret-Lutz
d0c296e1cf org: mention "make check" and the new GPG key
Fixes #515.

* doc/org/install.org: Here.
2022-10-10 10:06:25 +02:00
Alexandre Duret-Lutz
8131fae1a6 Release Spot 2.11
* NEWS, configure.ac, doc/org/setup.org: Update version.
2022-10-08 20:59:27 +02:00
Alexandre Duret-Lutz
51caa5588e update gitlab references
As LRDE is being renamed LRE, gitlab is one of the first URL to
migrate.  The old URL is still supported, but we want to only use the
new one eventually.

* .dir-locals.el, .gitlab-ci.yml, HACKING, NEWS, doc/org/concepts.org,
doc/org/install.org, doc/org/setup.org, elisp/Makefile.am,
elisp/hoa-mode.el, tests/ltsmin/README: Update to the new gitlab URL.
2022-09-23 08:57:57 +02:00
Alexandre Duret-Lutz
383128d983 * doc/tl/tl.tex: Fix a couple of typos detected by ispell. 2022-09-23 08:57:57 +02:00
Alexandre Duret-Lutz
c1c874b1a5 ltlsynt: add options --dot and --hide-status
* bin/ltlsynt.cc: Implement these options.
* bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt):
Make extern.
* NEWS: Mention the new options.
* doc/org/ltlsynt.org: Use dot output in documentation.
* tests/core/ltlsynt.test: Quick test of the new options.
2022-09-14 15:33:46 +02:00
Alexandre Duret-Lutz
d9248e2e97 * doc/org/concepts.org (T-based vs. S-based acceptance): Adjust example. 2022-09-12 14:15:05 +02:00
Alexandre Duret-Lutz
fe3ebd370b add the TACAS'22 reference
* doc/org/citing.org, doc/spot.bib: There.
2022-09-07 09:59:31 +02:00
Alexandre Duret-Lutz
2848951965 * doc/spot.bib: Add entries for last two tool papers. 2022-08-10 10:28:44 +02:00
Alexandre Duret-Lutz
a7e87a1fc7 Mention the CAV'22 paper
* doc/org/citing.org: Here.
* doc/org/spot.css: Add support for "begin_note...end_note".
2022-08-10 10:28:41 +02:00
Alexandre Duret-Lutz
de9041bb31 mealy: make output_assignment the default for reduce_mealy
* spot/twaalgos/mealy_machine.hh: Here. Also cite the FORTE paper.
* doc/spot.bib (renkin.22.forte): New entry.
2022-08-06 14:08:23 +02:00
Alexandre Duret-Lutz
b0165cf39c * doc/org/tut10.org: Use the same formula in C++ as in Python and sh. 2022-08-05 18:55:44 +02:00
Alexandre Duret-Lutz
3e2201bd80 tests: add figures from CAV'22 paper
* tests/python/cav22-figs.ipynb: New file.
* doc/org/tut.org, tests/Makefile.am: Add it.
2022-07-12 15:05:09 +02:00
Alexandre Duret-Lutz
23908f3d2f Add a --enable-pthread option to activate experimental threading code
* NEWS, README, doc/org/compile.org: Mention the option and
its effect on compilation requirements.
* configure.ac: Add the --enable-pthread option, and ENABLE_PTHREAD
macro.
* doc/org/g++wrap.in, spot/Makefile.am, spot/libspot.pc.in: Compile
with -pthread conditionally.
* spot/graph/graph.hh, spot/twa/twagraph.cc: Adjust the code to not
use thread-local variables, and let the pthread code be optional.
* .gitlab-ci.yml: Activate --enable-pthread in two configurations.
2022-06-21 09:56:13 +02:00
Alexandre Duret-Lutz
3b8e11322b Merge branch 'master' into next 2022-05-18 09:03:40 +02:00
Alexandre Duret-Lutz
e0de77d8a4 Release Spot 2.10.6
* NEWS, configure.ac, doc/org/setup.org: Set version to 2.10.6.
2022-05-18 08:52:33 +02:00
Alexandre Duret-Lutz
9ae2e9c03d Fix link to parity game example
Reported by Florian Renkin.

* doc/org/index.org: Here.
2022-05-18 07:07:26 +02:00
Alexandre Duret-Lutz
4a2bdd6e86 Fix link to parity game example
Reported by Florian Renkin.

* doc/org/index.org: Here.
2022-05-04 17:40:17 +02:00
Alexandre Duret-Lutz
73e148446c Merge branch 'master' into next 2022-05-03 09:05:26 +02:00
Alexandre Duret-Lutz
c70a06ae0a Release Spot 2.10.5
* NEWS, configure.ac, doc/org/setup.org: Update.
2022-05-03 08:59:17 +02:00
Alexandre Duret-Lutz
58f39ec287 * doc/org/tut40.org: Clarify, as suggested by a CAV'22 reviewer. 2022-05-02 17:24:23 +02:00
Alexandre Duret-Lutz
5f43c9bfce ltlsynt: implement --tlsf to call syfco automatically
Fixes #473.

* NEWS, doc/org/ltlsynt.org: Mention it.
* bin/common_trans.cc, bin/common_trans.hh (read_stdout_of_command):
New function.
* bin/ltlsynt.cc: Implement the --tlsf option.
* tests/core/syfco.test: New file.
* tests/Makefile.am: Add it.
2022-04-13 09:08:40 +02:00
Alexandre Duret-Lutz
a211bace68 autcross: implement --language-complemented
Suggested by Ondřej Lengál.  Fixes #504.

* bin/autcross.cc: Implement the --language-complemented option.
* NEWS, doc/org/autcross.org: Document it.
* tests/core/autcross.test: Test it.
* THANKS: Add Ondřej.
2022-04-06 15:38:23 +02:00