twaalgos: introduce match_states(a,b)

This is a useful part for issue #591.

* spot/twaalgos/matchstates.cc, spot/twaalgos/matchstates.hh: New
files.
* spot/twaalgos/Makefile.am: Add them.
* python/spot/impl.i: Add python bindings.
* tests/python/matchstates.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention this new function.
This commit is contained in:
Alexandre Duret-Lutz 2024-08-28 15:57:33 +02:00
parent b549e8e8c1
commit 5f1d00b858
7 changed files with 164 additions and 0 deletions

6
NEWS
View file

@ -56,6 +56,12 @@ New in spot 2.12.0.dev (not yet released)
were missing the rule "[*0]|f ≡ f" when f already accepts the
empty word. (Issue #545.)
- spot::match_states(A, B) is a new function that returns a vector
V such that V[x] contains all states y such that state (x, y) can
reach an accepting cycle in product(A, B). In particular, if A
and B accept the same language, any word accepted by A from state
x can be accepted in B from some state in V[x].
Bug fixes:
- Generating random formulas without any unary opertor would very