• Alexandre Duret-Lutz's avatar
    simulation: do not depend on bdd numbers for ordering classes · ae0e84ac
    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/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.
    ae0e84ac
simulation.cc 24.3 KB