-
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