Skip to content
  • Alexandre Duret-Lutz's avatar
    ltl2tgba: clear simplification cache between translations · aa404823
    Alexandre Duret-Lutz authored
    The cache used in formula simplification will keep atomic propositions
    defined between several translations, and may impact variable order.
    Reported by Maximilien Colange.
    
    * spot/tl/simplify.hh, spot/tl/simplify.cc,
    spot/twaalgos/translate.cc, spot/twaalgos/translate.hh (clear_cache):
    New method.
    * bin/ltl2tgba.cc, bin/ltl2tgta.cc: Call it.
    * spot/twaalgos/stats.cc: Do not keep a point to the formula after
    printing statistics.
    * tests/core/ltl2tgba.test: Add a test case.
    * tests/core/readsave.test: Adjust one formula.
    * NEWS: Mention the issue.
    aa404823