GitLab

* NEWS: Here.

Florian Renkin authored Apr 12, 2022 and Alexandre Duret-Lutz committed May 02, 2022

* bin/ltlsynt.cc: here

Libtool 2.4.7 breaks if AR_FLAGS contains a space. See
https://lists.gnu.org/archive/html/bug-libtool/2022-03/msg00009.html

* debian/rules: Use gcc-{nm,ar,ranlib} so we do not have to pass
the plugin explicitly.

Philipp Schlehuber authored Mar 29, 2022 and Alexandre Duret-Lutz committed May 02, 2022

Optimization in Zielonka failed
under certain circumstances
todo: Devise a specialized test
for direct attr computation

* spot/twaalgos/game.cc: Correction
* tests/python/game.py: Test

Florian Renkin authored Mar 21, 2022 and Alexandre Duret-Lutz committed May 02, 2022

* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: add tests

Reported by Florian Renkin.

* spot/graph/graph.hh (sort_edges_of): Fix invalid read when sorting a
state without successor.  Seen on core/tgbagraph.test.

Florian Renkin authored Mar 15, 2022 and Alexandre Duret-Lutz committed May 02, 2022

* bin/ltlsynt.cc: here

* python/spot/impl.i (formula_from_bdd): Instantiate for twa_graph.
* spot/twa/twa.hh (register_aps_from_dict): Typo in exception.
* tests/python/except.py: More tests for the above.
* tests/python/bdddict.py: Typo in comment.

Antoine Martin authored Mar 10, 2022 and Alexandre Duret-Lutz committed May 02, 2022

* tests/run.in: keep original PYTHONPATH contents
* NEWS: mention the bug

Partial fix for #501.

* tests/core/prodchain.test: Hardcode the seq output.
* tests/core/bricks.test: Use $AWK instead of seq.
* tests/core/defs.in: Define $AWK.
* NEWS: Mention the bug.

The fallback definition of SIZE_MAX supplied by flex was not
preprocessor friendly and prevented robin_hood.hh from doing "#if
SIZE_MAX == UINT64_MAX", as observed by Marc Espie on OpenBSD.

* spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Define
__STDC_VERSION__ just so that the code generated by Flex
include <inttypes.h>.
* NEWS: Mention the bug.
* THANKS: Add Marc.

* spot/twaalgos/parity.cc (reduce_parity): Use the
size of the edge vector to initialize piprime1 and piprime2,
not the number of edges.
* tests/python/parity.py: Add test case, based on a report
by Yann Thierry-Mieg.

These were deprecated in C++11, and are supposed to be removed from
C++17, however gcc-snapshot just started warning about those.

* spot/misc/bddlt.hh, spot/misc/hash.hh, spot/misc/ltstr.hh,
spot/twa/taatgba.hh, spot/twaalgos/ltl2tgba_fm.cc: Here.

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

Reported by Yechuan Xia

* python/spot/impl.i: Add %newobject to all __iter__ methods.
* NEWS: Mention the list of affected methods.
* THANKS: Update.

* NEWS, configure.ac, doc/org/setup.org: Update version.

The current building issue is a docker issue unrelated to Spot,
so it should not prevent us from doing a release.

* .gitlab-ci.yml (rpm-pkg): Allow failure.

Fixes #496.

* doc/org/init.el.in: Install org-mode from GNU ELPA.

* doc/spot.bib (blahoudek.16.atva, degiacomo.13.ijcai): New entries.
* spot/tl/ltlf.hh, spot/twaalgos/complement.hh: Use them.

* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Ignore edges
whose colors are not part of the colors gathered in the SCC up to
deciding acceptance.
* tests/python/genem.py: New test case, reported by Clément Tamines.
* THANKS: Add him.
* NEWS: Mention the bug.

The related GraphViz issue is
https://gitlab.com/graphviz/graphviz/-/issues/2179

* spot/twaalgos/dot.cc: Avoid initial newline in title.
* NEWS: Mention the bug.
* tests/core/det.test, tests/core/dstar.test,
tests/core/neverclaimread.test, tests/python/automata-io.ipynb: Adjust
test cases.

* bin/common_setup.cc, debian/copyright: Here.

Philipp Schlehuber authored Jan 07, 2022 and Alexandre Duret-Lutz committed Jan 14, 2022

Monitors can now be split AND completed at the same time.
Split can be called on games without providing
"synthesis-outputs" - relying on named prop.

* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Here

Reported by Reuben Rowe.

* spot/twaalgos/complement.cc (complement): Remove the hard-coded
simul=0 option on automata with >32 states.  In 2.10 simul=0 now
implies det-simul=0, causing the regression, and most importantly it
is not needed anymore, because we have other threashold like simul-max
and simul-trans-pruning in place.
* tests/core/complement.test: Add Reuben's automaton as test case.
* NEWS: Mention the fix.

This fixes #492, based on a report from Jérôme Dubois.

* spot/twaalgos/sbacc.cc: If the initial state is in a rejecting
component, start with an initial state whose colors are unsat_mark.
* tests/core/sbacc.test: Add test case.
* tests/python/pdegen.py: Adjust it.

* doc/tl/tl.tex: Here.

* doc/org/index.org, tests/python/bdditer.py: Here.

Philipp Schlehuber authored Dec 06, 2021 and Alexandre Duret-Lutz committed Jan 14, 2022

Isomorph but different machines were created
depending on ARM vs Intel

* spot/twaalgos/mealy_machine.cc: Fix here

* NEWS, configure.ac, doc/org/setup.org: Set version to 2.10.2.

Reported by Ayrat Khalimov.

* spot/tl/formula.hh (is_literal): Mark as const.

* spot/parsetl/scantl.ll: Diagnose delays (##n) larger than
unbounded().  Remove all checks for delays with 1 or 2 characters.
* tests/core/parseerr.test: Add a test case.
* NEWS: Mention this fix.