2026-10-16  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	Relase Spot 2.16.1

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

2026-10-15  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	translate: fix ltl-split handling of <-> and xor

	Fixes #662 reported by Tobias Meggendorfer.

	* NEWS: Mention the bug.
	* THANKS: Remove trailing dot.
	* spot/twaalgos/translate.cc (translator::run_aux): Fix ltl-split
	heuristic when dealing with <-> or xor.
	* tests/core/ltl2tgba2.test, tests/core/ltlsynt.test: Add test cases.
	* tests/python/games.ipynb: Regenerate.

2026-10-15  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	tl: always split OR/AND when testing implications

	Fixes #660.

	* spot/tl/simplify.cc (tl_simplifier_cache::syntactic_implication_aux,
	tl_simplifier_cache::syntactic_implication): When f or g is OR or AND,
	always break the implication instead of trying to use as_bdd() on the
	Boolean parts.
	* tests/core/ltlfilt.test: Add the test case from #660.
	* tests/core/bdddict.test, tests/core/ltlf.test: Adjust expected
	output.
	* NEWS: Mention the change.

2026-10-15  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	common: rename SPOT_make_shared_enabled__

	Names with `__` are reserved by the C++ standard.  Rename
	SPOT_make_shared_enabled__ as SPOT_make_shared_enabled_.

	* spot/ltsmin/ltsmin.cc, spot/misc/common.hh, spot/twa/taatgba.hh,
	spot/twa/twagraph.cc, spot/twa/twagraph.hh, spot/twa/twaproduct.hh,
	spot/twaalgos/couvreurnew.cc, spot/twaalgos/gtec/gtec.cc,
	spot/twaalgos/gv04.cc, spot/twaalgos/magic.cc, spot/twaalgos/se05.cc,
	spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc: Here.

2026-10-15  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	ltl2tgba_fm: deal with cland tidy warnings

	* spot/twaalgos/ltl2tgba_fm.cc: Fuse two cases to clear, and add some
	NOLINT comments to clear clang-tidy warnings.

2026-10-09  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	bin: remove %X from --help of LTL tools

	Using --stats=%x in tools that output LTL is a way to output the
	number of atomic propositions.  Using %X was never supported, but was
	documented because of a bad copy-paste.

	* bin/common_output.hh: Remove %X from --help.
	* doc/org/ltlfilt.org: Adjust.

2026-10-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	ltsmin: declare the members defined in spins_kripke.hxx inline

	spins_kripke.hxx is included by spins_kripke.hh, and is therefore seen
	by both spot/ltsmin/ltsmin.cc and the programs of tests/ltsmin.  None
	of the member functions it defines out of class carried the inline
	specifier, so all of them were emitted into every translation unit that
	included the header.

	When libspotltsmin is compiled (and linked) as a static library, the
	linker reports 24 duplicate symbols and neither
	tests/ltsmin/modelcheck nor tests/ltsmin/testconvert can be built at
	all, which also prevented "make check" from running the test suite.

	* spot/ltsmin/spins_kripke.hxx: Mark the member definitions of
	cspins_state_manager, cspins_iterator, and of the
	kripkecube<cspins_state, cspins_iterator> specialization as inline.

2026-10-09  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	* doc/org/tut50.org: Add missing class in plantuml diagram.

2026-10-08  Ondra Lengal  <ondra.lengal@gmail.com>

	toparity: do not assert that uncolored outputs have no edges

	to_parity_generator::run() asserted that if no edge of the output
	received a color, the input had no edges.  However, all edges are
	also left uncolored when all cycles of the input are rejecting: the
	SCCs are then processed in the "max even" world, where uncolored
	edges are rejecting.  For instance, to_parity() failed this
	assertion on a single state with a self-loop and acceptance "f".
	The output acceptance "f" chosen in that case is correct, so only
	the assertion and its comment were wrong.

	Fixes #659.

	* spot/twaalgos/toparity.cc (to_parity_generator::run): Remove the
	assertion and update the comment.
	* tests/python/toparity.py: Add test cases.
	* NEWS: Mention the bug.

2026-10-08  Ondra Lengal  <ondra.lengal@gmail.com>

	toparity: handle uncolored recursive results in try_parity_prefix()

	try_parity_prefix() asserted that the recursive processing of the
	SCCs left after removing the parity prefix produced at least one
	colored edge.  This is not the case when all of these edges stay
	uncolored, e.g., when all the remaining cycles are rejecting.  For
	instance, to_parity() failed this assertion on a 2-state automaton
	with acceptance "Fin(1) & Inf(0) & Inf(2)".

	An uncolored edge behaves like color -1, which is odd.  The code
	following the assertion already computed this parity when
	max_scc_color_rec is 0, but only through the wrap-around of
	"max_scc_color_rec - 1" on unsigned integers.

	Fixes #658.

	* spot/twaalgos/toparity.cc (to_parity_generator::try_parity_prefix):
	Remove the assertion, and handle a max_scc_color_rec of 0
	explicitly.
	* tests/python/toparity.py: Add a test case.
	* NEWS: Mention the bug.
