-
Alexandre Duret-Lutz authored
functionality of the old tgba_tba_proxy. * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator, tgba_tba_proxy): Rewrite to produce TBA with at most N copies of each state, skipping the `bddtrue' stage now used only in tgba_sba_proxy. Doing so removes approximately 6% of states in the degeneralized tests of spotlbtt.test. (tgba_sba_proxy): Implement it. * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust to take a tgba_sba_proxy. * src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to never_claim_reachable().
cac85dbc