Fixes#401, reported by Victor Khomenko.
* spot/twaalgos/stutter.cc (sl, sl2): If {} is accepting, upgrade the
acceptance condition.
* tests/python/stutter.py: Add test cases.
Reported by Juraj Major.
* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Do not
assume TRACK_STATES is enabled.
* tests/core/autcross5.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
* spot/twaalgos/genem.cc: If a disjunct has no unit-Fin to remove the
code should select any Fin occuring in the disjunct, but it was
selecting any Fin occuring in the acceptance condition (made of
disjuncts) instead. This could potentially double the number of
recursive calls.
* spot/twaalgos/relabel.cc: Remove false transitions if
some of the propositions are equivalent to true or false.
* NEWS: Mention the bug.
* tests/core/ltl2tgba2.test: Test it.
Reported by František Blahoudek.
* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.
Reported by František Blahoudek.
* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.
* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error. Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.
This fixes a complementation bug reported by Juraj Major and Tereza
Šťastná.
* spot/twaalgos/remfin.cc (is_scc_tba_type): Fix the condition for
handling Fin-alone pairs.
* tests/core/complement.test: Add Juraj & Tereza's test case.
* NEWS: Mention it.
This is to workaround differences in minidom's pretty-printing that
occurred between Python 3.7 and 3.8.
* python/spot/jupyter.py (SVG): New class.
* python/spot/__init__.py: Use it.
* tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/automata.ipynb, tests/python/formulas.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb: Adjust.
* spot/twa/acc.hh (acc_cond::mark_t): Diagnose mark_t with set numbers
that are too larges.
* tests/python/except.py: Adjust.
* tests/core/acc.cc: Remove most of asserts, as those can be disabled,
and adjust expected exception.