Skip to content
  • Damien Lefortier's avatar
    Add an algorithm (from Couvreur) working on BDDs to reduce the · edd4b2b5
    Damien Lefortier authored
    size of TGBAs represented as BDDs by deleting unaccepting SCCs.
    
    * src/eltlparse/eltlparse.yy: Remove a warning.
    * src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
    src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
    new function delete_unaccepting_scc in both classes.
    * src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
    new function in LaCIM for ELTL and bench it.
    * src/tgbatest/defs.in: Fix it.
    * bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
    ELTL in benchs.
    edd4b2b5