• Alexandre Duret-Lutz's avatar
    * src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the · cac85dbc
    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
neverclaim.cc 4.58 KB