bdd_has_common_assignement determines if two bdds a and b
have (at least) one common assignement.
That is it will return true iff bdd_and(a, b) != bddfalse.
* src/bddx.h: Here
* src/bddop.c: Here
* spot/twa/twagraph.cc (merge_states): Return the number
of removed states, and use that to decide if defrag_states
is needed.
* spot/twa/twagraph.hh, NEWS: Document that.
* tests/core/tgbagraph.test, tests/core/twagraph.cc: Adjust test case.
Fixes#468.
* python/spot/__init__.py: Add wrapper around twa::acc() and
twa::get_acceptance() to store the automaton into the acceptance
proxy, therefore ensuring that the automaton survives that proxy.
* tests/python/setacc.py: Test it.
It was noted in #470 that make_twa_graph did not copy named
properties. Let's fix that.
* spot/twa/twa.hh, spot/twa/twa.cc (copy_named_properties_of): New
method.
* spot/twa/twagraph.hh (make_twa_graph): Add an extra argument to
call copy_named_properties_of() optionally.
* python/spot/__init__.py (twa_graph.__copy__): Use it.
* tests/python/twagraph.py: Test that.
* tests/sanity/namedprop.test: Ensure copy_named_properties_of copies
all known named properties.
Fixes#470, suggested by Cambridge Yang.
* python/spot/__init__.py (twa_graph.__copy__): Call make_twa_graph.
* tests/python/twagraph.py: Test it.
* NEWS: Mention it.
Fixes#471, reported by Cambridge Yang.
* spot/twa/twa.cc (intersecting_run): Disable the product
optimization for weak automata.
* tests/python/471.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
Part of #471.
* spot/twaalgos/emptiness.cc: Throw an exception if
the cycle is rejecting.
* spot/twaalgos/emptiness.hh: Document this behavior.
* tests/python/except.py: Test it.
This fixes#469.
* spot/misc/bitset.hh (bitset::operator-): Rewrite.
I cannot follow the logic of the old implementation.
* tests/python/setacc.py: Add a test case, inspired from #469.
Part of #467.
* tests/python/bdddict.py, tests/python/ltl2tgba.py,
tests/python/ltlparse.py, tests/python/ltlsimple.py,
tests/python/sccinfo.py, tests/python/simstate.py,
tests/python/split.py, tests/python/tra2tba.py: Adjust to
deal with a non-refcounted Python implementation.
This implement the suggestion is issue #467 but the test suite is
still not completely passing with pypy3.
* m4/pypath.m4: Detect the suffix for extensions.
* python/Makefile.am: Use it.
* tests/run.in: Recognize pypy3 as a Python version.
This fixes#462.
* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Replace the
redirect_src vector by a unique_ptr<unsigned[]>. Not only does this
remove the false positive diagnostic, but it also removes the unneeded
default initialization of the elements of that vector.
* src/bddx.h, misc/bddlt.hh (bdd_stable_cmp): Define this
new function, based on some code that was implemented in Spot, but was
unnecessarily doing reference counting.
* spot/twa/twagraph.cc: Implement it.
* spot/twa/twagraph.hh, NEWS: Document it.
* tests/python/mergedge.py: Test it.
* tests/core/ltlsynt.test, tests/python/games.ipynb: Adjust expectations.
* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization. It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
