2026-11-03  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	Release Spot 2.16.2

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

2026-11-02  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

	ltl2tgba_fm: deprecate the unsound simplifier argument

	The simplifier argument of ltl_to_tgba_fm() (and of the newer
	ltl_to_tgba_fm_otf()) used to simplify the LTL formula representing
	each state of the automaton before computing its successors.  This is
	unsound: a simplifier may rewrite a destination in a way that moves a
	promise under a temporal operator (Xd & FG!d becomes X(d & FG!d)),
	while the acceptance marks put on a transition are collected from the
	unsimplified destination.  The promise is then never charged in the
	state where it should be, and the automaton accepts too much.

	This option sat unused for years, until version 2.16 changed
	ltl_satisfiable() to explore the automaton on-the-fly, and this caused
	G(b -> XXd) & Gb & FG!d to be reported as satisfiable.

	Fixes #663, reported by Ben Andrew.

	* spot/twaalgos/ltl2tgba_fm.cc: Remove impl::dest_simplifier, and stop
	simplifying the destination formulas in succ_as_edges() and
	succ_as_acc_and_dest(); a caller-supplied simplifier is now only
	applied to the input formula.
	* spot/twaalgos/ltl2tgba_fm.hh: Document the deprecation of the
	simplifier argument of ltl_to_tgba_fm() and ltl_to_tgba_fm_otf(),
	with the Xd & FG!d counterexample.
	* spot/tl/sat.cc (otf_satisfiable): Do not pass a simplifier to the
	explorer.
	* tests/python/ltlsimple.py: Check that G(b -> XXd) & Gb & FG!d is
	unsatisfiable.
	* tests/core/ikwiad.cc: Drop the -fr option, now equivalent to the
	default.
	* tests/core/spotlbtt.test: Drop the two disabled algorithms using -fr.
	* NEWS: Mention the deprecation and the bug fix.
	* THANKS: Add Ben.

2026-11-02  Alexandre Duret-Lutz  <adl@lre.epita.fr>

	* bin/spot-x.cc: Fix "acd" doc.

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

	* NEWS, configure.ac: Bump version.

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.
