* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: add detection
of edges that are in at least one accepting cycle.
* spot/twaalgos/toparity.cc,
spot/twaalgos/toparity.hh: add parity_type_to_parity and
buchi_type_to_buchi.
When n is an int, doing "new formula[n];" gives us "warning: argument 1
value '18446744073709551615' exceeds maximum object size
9223372036854775807" on Red Hat.
* spot/gen/formulas.cc (pps_arbiter): Pass n as unsigned. Also
fix some determinism in the strict variant.
* utf8/LICENSE, utf8/utf8/cpp11.h, utf8/utf8/cpp17.h: New files.
* Makefile.am: Distribute them.
* utf8/README.md, utf8/utf8/checked.h, utf8/utf8/core.h,
utf8/utf8/unchecked.h: Update to the current version of utfcpp.
* README: Add a link to the upstream github.
This should fix compilation on OSX, as reported by Yann Thierry-Mieg.
* m4/environ.m4: New file.
* m4/gnulib-cache.m4, m4/gnulib-comp.m4: Update.
* bin/common_trans.cc [HAVE_SPAWN_H]: Do not define environ.
* spot/twaalgos/game.cc: solve_parity_game now works for any of
the four parity types and partially colored graphs.
Also removing unnescessary steps from Zielonka.
h: Update
* tests/python/game.py: Update and additional tests
* tests/python/except.py: Remove outdated exception
Fixes#509.
* spot/parseaut/scanaut.ll: Reset ->str whenever a [ is read,
so that we do not attempt to clear ->str while reading garbage.
* NEWS: Mention the bug.
* tests/core/parseaut.test: Test it.
* spot/graph/graph.hh: Use a temporary array to store the destination
vector if the passed range belong to the dests_ vector. Otherwise the
passed begin/end risk being invalidated when dests_ is reallocated.
* NEWS: Mention the bug.
This was triggered by a question from Pierre Ganty on the mailing
list.
* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc (contains):
Generalize second argument to const_twa_ptr instead of
const_twa_graph_ptr.
* NEWS: Mention this.
* tests/python/ltsmin-pml.ipynb: Show that it work.
* THANKS: Mention Pierre.
* bin/common_file.cc, bin/common_file.hh (output_file): Add a
force_append option.
* bin/ltlsynt.cc: Implement the --from-pgame option, and
fix suppot for --csv when multiple inputs are processed.
* NEWS: Mention the new option.
* tests/core/syfco.test: Add a test case.
* tests/core/ltlsynt-pgame.test: New file.
* tests/Makefile.am: Add it.
* bin/common_finput.cc, bin/common_finput.hh: Add support for
process_tlsf_file.
* bin/ltlsynt.cc: Implement it.
* tests/core/syfco.test: Adjust test case.
* bin/common_finput.cc, bin/common_finput.hh,
bin/common_hoaread.hh (process_file): Split into...
(process_ltl_file, process_aut_filt): ... these, as we will need both
in ltlsynt.
* NEWS, README, doc/org/compile.org: Mention the option and
its effect on compilation requirements.
* configure.ac: Add the --enable-pthread option, and ENABLE_PTHREAD
macro.
* doc/org/g++wrap.in, spot/Makefile.am, spot/libspot.pc.in: Compile
with -pthread conditionally.
* spot/graph/graph.hh, spot/twa/twagraph.cc: Adjust the code to not
use thread-local variables, and let the pthread code be optional.
* .gitlab-ci.yml: Activate --enable-pthread in two configurations.
As discussed with Jan Strejček.
* spot/twa/acc.cc, spot/twa/acc.hh (fin_unit_one_split): New function.
(fin_one_extract): Return the simplified acceptance condition as an
optimization.
* python/spot/impl.i: Bind this new function.
* tests/python/acc.py: New file, to test it.
* tests/Makefile.am: Add acc.py.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Implement the
spot211 variant of the emptiness check.
* tests/python/genem.py: Test it.
* tests/python/acc_cond.ipynb: Adjust test for fin_one_extract.
With a formula like G(b1) & (GFi <-> GF(b1)), a direct strategy was
created while it is unrealizable.
* spot/twaalgos/synthesis.cc: here.
* tests/core/ltlsynt.test: add tests
merge_states is now hash-based, uses the new edge-sorting with
src first and can be executed in parallel.
* spot/twa/twagraph.cc: Here
* tests/python/mergedge.py: Test
sort_edge_srcfirst_ will sort the edge with respect
to the src state, then sort each sub list with respect
to the given predicate, possibly in parallel.
* spot/graph/graph.hh: Here
This largely speeds up the computation for conditions
like "Rabin n" sharing a lot of subtrees.
Also implement options to stop the construction if the shape is wrong.
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Implement the
cache and the options.
* tests/python/zlktree.ipynb, tests/python/zlktree.py: New tests.
* 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.
