• Alexandre Duret-Lutz's avatar
    ltlcross: adjust to work with generic acceptance · 717c8577
    Alexandre Duret-Lutz authored
    * src/bin/ltlcross.cc: Remove Fin-acceptance before
    doing checks.  More --verbose output.
    * src/tgba/acc.cc, src/tgba/acc.hh: Add an eval_sets() function
    to find the set of acceptance sets needed to satisfy the condition
    in an accepting SCC.
    * src/tgbaalgos/gtec/ce.cc: Use eval_sets() when computing
    a counter example.
    * src/tgbaalgos/gtec/gtec.cc: Raise an exception when called
    on an acceptance that contains Fin.
    * src/tgbatest/ltl2dstar3.test, src/tgbatest/ltlcrossce2.test:
    New files.
    * src/tgbatest/Makefile.am: Add them.
    * src/tgba/tgba.cc (is_empty): Call remove_fin if needed.
    * src/tgbaalgos/product.cc, src/tgbaalgos/dtgbacomp.cc: Adjust
    to work with generic acceptance.
    717c8577
acc.cc 9.74 KB