On 32bit archetectures, long int = int the current check for detecting
values that overflow int will fail.  Conversion routings should check
errno.

* bin/common_conv.cc, bin/common_range.cc: Here.

Fixes #523.

* bin/autfilt.cc: Remove the restriction.
* tests/core/acc_word.test: Add test case.
* NEWS: Mention the fix.

Florian Renkin authored Jan 20, 2023 and Alexandre Duret-Lutz committed Jan 23, 2023

* bin/ltlsynt.cc: here

* bin/common_setup.cc: Here.

* spot/priv/robin_hood.hh: Update.
* spot/priv/Makefile.am: Patch ROBIN_HOOD_IS_TRIVIALLY_COPYABLE to
work around an issue with clang on Arch linux.

Fixes #524, reported by Rüdiger Ehlers.

* spot/twaalgos/dbranch.cc: When merging an edge going to state
without successors simply delete it.
* bin/spot-x.cc: Typo in documentation.
* tests/core/ltlcross.test: Add a test case.
* NEWS: Mention the bug.

* bin/common_file.cc, bin/common_file.hh, bin/common_finput.cc,
bin/common_finput.hh, bin/common_output.cc, bin/common_setup.cc,
bin/common_setup.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc,
bin/ltlsynt.cc, bin/randltl.cc: Fix minor code issues reported by
sonarcloud.

* bin/common_conv.cc (to_int, to_unsigned): Here.
* bin/common_range.cc (parse_range): And there.
* tests/core/ltlgrind.test, tests/core/genaut.test,
tests/core/randaut.test: Add test cases.

* bench/dtgbasat/gen.py, bin/autcross.cc, bin/autfilt.cc,
bin/common_aoutput.cc, bin/common_aoutput.hh: Various cleanups.

* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/simulation.cc: Simplify, as reported by sonarcloud.

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.

Fixes #522 reported by Raven Beutner.

* spot/parseaut/parseaut.yy: Make sure all edges leaving
the initial state have the same color.
* THANKS: Add Raven.
* NEWS: Mention the bug.
* tests/core/522.test: New file.
* tests/Makefile.am: Add it.

* spot/twaalgos/determinize.cc (sorted_nodes): Rewrite to
avoid reallocation of temporary vector.

* spot/priv/allocator.hh: Delete.
* spot/priv/Makefile.am, tests/core/mempool.cc: Adjust.

* python/spot/__init__.py (acd): Rewrite javascript so that it does
not use jQuery, to make it easier to use in jupyterlab, or with
nbconvert.
* tests/python/zlktree.ipynb: Adjust.
* NEWS: Mention this.

Evaluate incomp of player conditions only if necessary

* spot/twaalgos/mealy_machine.cc: Here

Put the new function to use in order to speed up
mealy machine minimization

* spot/twaalgos/mealy_machine.cc: Here
* spot/twaalgos/synthesis.cc
, spot/twaalgos/synthesis.hh: Helper function to relabel games
* tests/python/_mealy.ipynb
, tests/python/except.py
, tests/python/_partitioned_relabel.ipynb: Adapt/expand tests

Function taking an automaton and trying to relabel
it by partitioning the old conditions and encode the
different subsets of the partition with new variables

* spot/priv/Makefile.am: Add
* spot/priv/partitioned_relabel.hh
, spot/priv/partitioned_relabel.cc: try_partition_me,
computes the partition of a given vector of bdds
* spot/twaalgos/relabel.hh
, spot/twaalgos/relabel.cc: Here. Adapt also relabel()
to cope with the different type of relabeling_maps
* tests/python/_partitioned_relabel.ipynb
, tests/python/except.py: Test and Usage
* tests/Makefile.am: Add test

* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.3.

* spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh,
spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help
g++.

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

* spot/tl/formula.hh, spot/tl/formula.cc (one_plus): New.
(fnode): Add a saturated argument.
(tt_, ff_, eword_, one_plus, one_star): Create saturated node.
(destroy): Do not check for id() < 3.

* 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.

Philipp Schlehuber authored Nov 27, 2022 and Alexandre Duret-Lutz committed Dec 06, 2022

When calling solve_parity_game() multiple times on the same
automaton the strategies are appended one after the other.
Reported by Dávid Smolka.

* NEWS: Mention the bug.
* spot/twaalgos/game.cc: Fix it.
* tests/python/game.py: Test it.
* THANKS: Add Dávid.

Philipp Schlehuber authored Dec 01, 2022 and Alexandre Duret-Lutz committed Dec 06, 2022

* spot/twaalgos/mealy_machine.cc (minimize_mealy): Do not compare
result to the original unsplit machine without splitting it first.
* tests/python/mealy.py: Add a test case.

* m4/getopt.m4: Pretend sys/cdefs.h is missing, so that Alpine linux
does not output a warning which we would turn into an error.

* bin/autfilt.cc: If -c is used, print the match_count even
in present of parse errors.
* tests/core/readsave.test: Adjust.
* NEWS: Mention the bug.

Reported by Pierre Ganty.

* spot/parseaut/parseaut.yy: Add diagnostics.
* tests/core/parseaut.test: Adjust expected output, and add a test
case.
* NEWS: Mention the bug.

Fixes #512.

* configure.ac: Here.
* NEWS: Mention the bug.

This issue surfaced in twacube.test after the previous patches.

* spot/twaalgos/ltl2tgba_fm.cc: Release the formula namer on abort.
* NEWS: Mention the bug.

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.

For issue #521, reported by Jacopo Binchi.

* spot/tl/simplify.cc: Here.
* tests/core/521.test: New test case.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
* THANKS: Add Jacopo Binchi.

* spot/misc/satsolver.hh, spot/tl/formula.hh, spot/twaalgos/hoa.hh,
spot/twaalgos/synthesis.hh, spot/twaalgos/zlktree.hh,
spot/twacube_algos/convert.hh: Typos in Doxygen comments.