Jérôme Dubois authored Nov 20, 2021 and Alexandre Duret-Lutz committed Nov 22, 2021

* spot/kripke/kripkegraph.hh, spot/misc/hash.hh, spot/twa/taatgba.cc,
  spot/twa/twagraph.hh, tests/core/ngraph.cc: Replace subtraction of
  pointeur minus nullptr by an explicit cast to size_t.
* spot/twa/acc.hh: Add explicit default copy assignment operator for
  rs_pair.

Reported by Yuri Victorovich, on FreeBSD.

* configure.ac: Test for them.
* spot/mc/mc_instanciator.hh: Only use them if they are present.
* NEWS: Mention the fix.

* spot/twa/twagraph.cc (purge_dead_states): Be bddfalse-aware!
* spot/twa/twagraph.hh, NEWS: Document this.
* tests/python/alternating.py, tests/python/twagraph.py: Add some
test cases.

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

* spot/twaalgos/sbacc.cc (sbacc): Define the original-states
property on the created automaton.
* spot/twaalgos/sbacc.hh: Improve documentation.
* tests/python/sbacc.py: Update test cases.

For issue #485.

* spot/tl/formula.cc, spot/tl/formula.hh: Catch min/max overflow
when the operators are constructed.  Also disable travial
simplification rules that would create such overflow.
For instance x[*200][*2] will not become x[*400] anymore.
* python/spot/impl.i: Catch std::overflow_error.
* tests/core/equals.test, tests/python/except.py: Add test cases.

* spot/twaalgos/mealy_machine.cc (is_split_mealy_specialization): Hide
spl in NDEBUG.
* spot/twaalgos/synthesis.cc (apply_strategy): sp is not always used.

For issue #485.

* spot/parsetl/parsetl.yy: Add a diagnostic.
* tests/core/parseerr.test: Test it.

Fixes #488.

* configure.ac: Fix --enable-doxygen's help text, and add
one for --enable-warnings.

* tests/Makefile.am (ltsmin_modelcheck_LDADD,
ltsmin_testconvert_LDADD): Add libbddx as a dependecy.

* python/Makefile.am: Define __STDC_FORMAT_MACROS.

* bin/ltlsynt.cc: Change "sd" to "lar" as default algorithm in the doc.

* NEWS, README, HACKING, doc/org/install.org, m4/pypath.m4: Adjust.

Newer Jupyter version are able to capture the system's stdout and
stderr to display it in the notebook.  This is done asynchronously,
with a thread polling those file descriptor.  While this will help us
debug (finaly we can see the tracing code we put in C++) this causes
two issues for testing.  One is the asynchronous behaviour, which
makes it very hard to reproduce notebooks.  The second issue is that
older version of Jupyter used to hide some of the prints from the
notebook, so it is hard to accommodate both.

In the case of the ltsmin-pml notebook, loading the PML file from
a filename used to trigger a compilation silently (with output on the
console, but not in the notebook).  The newer version had the output
of that compilation spread into two cells.

* python/spot/ltsmin.i: Work around the issue by triggering the
compilation from Python, and capturing its output explicitly, so it
work with all Jupyter versions.  Also adjust to use the more recent
and simpler subprocess.run() interface, available since Python 3.5.
* tests/python/ltsmin-pml.ipynb: Adjust expected output.
* tests/python/ipnbdoctest.py (canonicalize): Adjust patterns.

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

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

* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc: Fix prototypes, as
well as several error messages.
* python/spot/impl.i: Implement an ad-hoc conversion for
std::vector<const_twa_graph_ptr>.
* tests/python/synthesis.ipynb: Use it to simplify the example.
Adjust some comments.

"Strategy" was used for mealy machines and game strategies a like.
Introduced the notion of mealy machine in three different flavors:
mealy machine: twa_graph with synthesis-outputs
separated mealy machine: mealy machine and all transitions
have conditions of the form (bdd over inputs)&(bdd over outputs)
split mealy machine: mealy machine that alternates between
env and player states. Needs state-players

* bin/ltlsynt.cc: renaming
* python/spot/impl.i: Add vector for const_twa_graph_ptr
* spot/twaalgos/aiger.cc,
spot/twaalgos/aiger.hh: Adapting functions
* spot/twaalgos/mealy_machine.cc,
spot/twaalgos/mealy_machine.hh: Add test functions and
propagate properties correctly. Adjust for names
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh: Removing unnecessary functions
and adapt to new names
* tests/python/aiger.py,
tests/python/_mealy.ipynb,
tests/python/mealy.py,
tests/python/synthesis.ipynb: Adjust

* bin/ltlsynt.cc: Here

* spot/twaalgos/zlktree.cc (acd_transform_sbacc): Fix the
acceptance condition when colored is true.
* tests/python/zlktree.py: Add test case.

* tests/python/acc_cond.ipynb, tests/python/contains.ipynb,
tests/python/decompose.ipynb, tests/python/games.ipynb,
tests/python/randltl.ipynb, tests/python/synthesis.ipynb,
tests/python/testingaut.ipynb: here.

* spot/tl/dot.cc: Show the min/max argument for Star/FStar nodes.
* tests/python/formulas.ipynb: Adjust test.

* src/bddop.c: Improve here
* src/bddtest.cxx: Tests here

* src/bddop.c: Fix is_cube with bddtrue as input
* src/bddtest.cxx: Add tests here

* examples/bddtest/bddtest.cxx: reset some global BDDs to avoid
issues when they are destroyed after BuDDy.

* examples/bddtest/Makefile.am, src/Makefile.am (TESTS):
Add this variable.
* examples/bddtest/bddtest.cxx: Return non-zero on error.

Fixes #480.

* bin/common_trans.cc (shorthands_ltl, shorthands_autproc): Write
those lists using regexes.  Add entries for Owl 21.0.
(show_shorthands, tool_spec): Adjust to use those regexes.
* doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org:
Update the list of shorthands.
* tests/core/ltldo.test: Add a couple of tests.
* NEWS: Mention this new feature.