Commit graph

5 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
ae0e84ac9e 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/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/highlighting.ipynb,
tests/python/piperead.ipynb, tests/python/testingaut.ipynb,
tests/python/word.ipynb: Update test cases for new order of states.
2017-06-03 10:03:59 +02:00
Alexandre Duret-Lutz
7b6cfd448c dot: fix printing of alternating automata
Related to #208.

* spot/twaalgos/dot.cc: Fix missing definitions of universal nodes,
and inclusion of universal nodes inside of SCC when none of the
destination comes back to the SCC.
* tests/python/_altscc.ipynb: Adjust and add more test cases.
* tests/core/alternating.test, tests/core/neverclaimread.test,
tests/core/readsave.test, tests/core/sccdot.test,
tests/python/decompose.ipynb: Adjust test cases.
* NEWS: Mention the bug.
2017-06-02 11:38:43 +02:00
Arthur Remaud
f7bbfd2812 autfilt: Better display of cluster when universal edge loops in it
Fixes #208

* NEWS: Informations about the modifications
* spot/twaalgos/dot.cc (print): Gestion of cluster for
universal transitions
* tests/core/alternating.test: tests added
* tests/core/neverclaimread.test: tests changed for
new dot format
* tests/core/readsave.test: tests changed
* tests/core/sccdot.test: tests changed
* tests/python/_altscc.ipynb: tests changed
* tests/python/decompose.ipynb: tests changed
2017-02-16 18:53:18 +01:00
Alexandre Duret-Lutz
215fcb799a Make spot.py a python package instead of a module
* python/spot.py, python/spot_impl.i: Rename as...
* python/spot/__init__.py, python/spot/impl.i: ... these.
* python/Makefile.am, tests/run.in: Adjust for new paths.
* tests/python/automata-io.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/piperead.ipynb,
tests/python/testingaut.ipynb: Adjust messages to refer to spot.impl
instead of spot_impl.
2016-01-26 19:20:26 +01:00
Alexandre Duret-Lutz
5cb94a1a3f Merge the core and python tests in the tests/ directory
* tests/: Rename as...
* tests/core/: ... this.
* python/tests/: Rename as...
* tests/python/: ... this.
* python/tests/run.in: Move as...
* tests/run.in: This, and adjust.
* tests/Makefile.am: Adjust to run both core and python tests.
* configure.ac, README, debian/python3-spot.examples, debian/rules,
doc/org/tut.org, python/Makefile.am, spot/ltsmin/Makefile.am,
spot/ltsmin/kripke.test, spot/sanity/ipynb.test: Adjust.
2016-01-04 16:02:30 +01:00
Renamed from python/tests/decompose.ipynb (Browse further)