Include script to heuristically remove accepting edges in Büchi automata
Enclosed is a script by @adl that removes, heuristically, accepting edges in a Büchi automaton. Removing accepting transitions is important (even crucial) for the performance of the FORQ-based inclusion algorithm. Fewer accepting edges means fewer fixpoints computed by the FORQ-based inclusion algorithm. I think it is important to include, in the next Spot release, this step removing accepting edges either as a script like the one below or natively.
import sys
import spot
def minimizeADL(aut):
assert aut.acc().is_buchi()
# If the automaton was state-based, we may lose that.
aut.prop_state_acc(spot.trival.maybe())
# Also if it was weak ( #562 )
aut.prop_weak(spot.trival.maybe())
testacc = spot.acc_cond(2, "Fin(0)&Inf(1)")
one = spot.mark_t([1])
zero = spot.mark_t([0])
none = spot.mark_t([])
si = spot.scc_info(aut)
for e in aut.edges():
# TO BE TESTED
#if not e.acc.has(zero):
# continue
srcscc = si.scc_of(e.src)
if srcscc != si.scc_of(e.dst): # transient edge
e.acc = none
elif si.is_rejecting_scc(srcscc):
e.acc = none
else:
e.acc = one
if spot.generic_emptiness_check_for_scc(si, srcscc, testacc):
e.acc = none
else:
e.acc = zero
if __name__ == '__main__':
if len(sys.argv) != 2:
sys.stderr.write("Usage: python less-tba.py <automaton.hoa>\n")
sys.exit(9)
hoafile = sys.argv[1]
spot.setup()
aut = spot.automaton(hoafile)
minimizeADL(aut)
outfile = hoafile + ".baccmin"
aut.save(outfile)