Skip to content
  • Alexandre Duret-Lutz's avatar
    simulation: do not depend on bdd numbers for ordering classes · 9ab4b840
    Alexandre Duret-Lutz authored
    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.
    9ab4b840