* spot/twaalgos/complete.hh: Adjust documentation.
* spot/twaalgos/complete.cc: If the acceptance condition is a
tautology, delay the forcing of Büchi acceptance until we are sure it
is needed.
* NEWS: Mention the change.
The issue seems to be inside std::vector's copy constructor, but it
highlighted places in Spot were we could avoid this copy.
* spot/twaalgos/ltl2taa.cc: Avoid some copies of std::vector<formula>.
Fix#505, Reported by Edmond Irani Liu.
* spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way.
* spot/twaalgos/hoa.cc: Do not force the use of named-states since
when the input is a kripke_graph.
* tests/python/kripke.py: Adjust test cases.
* NEWS: Mention the change.
* THANKS: Add Edmund.
The issue seems to be inside std::vector's copy constructor, but it
highlighted places in Spot were we could avoid this copy.
* spot/twaalgos/ltl2taa.cc: Avoid some copies of std::vector<formula>.
This will later help improve the handling of different input types of
ltlsynt.
* bin/common_finput.hh (job_type): New enum.
(job::type): Use it.
* bin/autcross.cc, bin/autfilt.cc, bin/common_finput.cc,
bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc,
bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc: Adjust
to use the job_type enum instead of a boolean.
Fix#505, Reported by Edmond Irani Liu.
* spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way.
* spot/twaalgos/hoa.cc: Do not force the use of named-states since
when the input is a kripke_graph.
* tests/python/kripke.py: Adjust test cases.
* NEWS: Mention the change.
* THANKS: Add Edmund.
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
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.
* 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.
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.