Skip to content
  • Alexandre Duret-Lutz's avatar
    * src/ltlvisit/contain.hh, src/ltlvisit/contain.cc (reduce_tau03): · d4c9bf2b
    Alexandre Duret-Lutz authored
    New function, performing LTL reduction a la tauriainen.03.a83.
    * src/ltltest/equals.cc, src/ltltest/reduc.cc: Add support for
    the new reduction.
    * src/ltltest/reduc.test: Cut the test in half, and additionally
    test the new reduction.
    * src/ltltest/reduccmp.test: Run on the new reduction.
    * src/ltltest/Makefile.am: Adjust.
    * src/tgbatest/ltl2tgba.cc: Add new options to apply the reduction.
    * src/tgbatest/spotlbtt.test: Use them.
    d4c9bf2b