Commit graph

3 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
9ab4b840fd simulation: do not depend on bdd numbers for ordering classes
Fixes #262 again.  Reported by Maximilien Colange.

* spot/twaalgos/simulation.cc: Use state numbers to order classes, not
their signatures.  The problem was that even if two simulation of the
same automaton assign the same signature, the BDD identifier used for
that signature might be different, and therefore the ordering obtained
by using BDDs as keys in a map can be different.  A side-effect of
this change is that the order of states in automata produced by
simulation-based reduction may change; many tests had to be updated.
* tests/core/ltl2tgba.test: Add a new test case based on Maximilien's
report.
* tests/core/complement.test, tests/core/det.test,
tests/core/parseaut.test, tests/core/prodor.test, tests/core/scc.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/decompose_scc.py,
tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
tests/python/sccinfo.py, tests/python/simstate.py,
tests/python/testingaut.ipynb, tests/python/word.ipynb: Update
test case for new order of states.
2017-06-02 14:10:34 +02:00
Alexandre Duret-Lutz
8e19d3f47e scc_info: introduce edges_of() and inner_edges_of()
This is motivated by some upcoming patch by Heňo.

* spot/twaalgos/sccinfo.hh (edges_of, inner_edges_of): New methods.
* spot/twaalgos/sccinfo.cc, spot/twaalgos/strength.cc: Use them.
* spot/twa/twagraph.hh (edge_number): Add an overload.
* python/spot/impl.i: Bind the new methods.
* tests/python/sccinfo.py: Add tests.
* NEWS: Mention the changes.
2017-05-09 22:12:42 +02:00
Alexandre Duret-Lutz
289b2383ad scc_info: add Python bindings
Related to #172, where we discussed that scc_info bindings were
missing.

* spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
(spot::scc_info_node): ... here to help Swig.
* python/spot/impl.i: Add bindings for scc_info.
* tests/python/sccinfo.py: New file.
* tests/Makefile.am: Add it.
2017-02-20 14:31:16 +01:00