Skip to content
  • Alexandre Duret-Lutz's avatar
    "ltl2tgba -Rm" will apply WDBA-minimization only if correct. · 54e10c25
    Alexandre Duret-Lutz authored
    * src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
    it is correct. Either we can quickly determine that a formula or
    its negation is a safety formula, or we can slowly check the
    equivalence of the WDBA-minimized automaton and the original
    automaton.
    * src/tgbatest/wdba.test: New test.
    * src/tgbatest/safety.test: Adjust comment.
    * src/tgbatest/spotlbtt.test: Use -Rm.
    * src/tgbatest/Makefile.am (TESTS): Add wdba.test.
    54e10c25