Alexandre Duret-Lutz (7ac570fa) at 27 Mar 23:13
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. The less accepting edges the faster 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)
CentOS 7 is still alive (it's used on the StarExec server, which is used for SyntComp), and still uses Python 3.6. So we can at least upgrade our requirements to Python 3.6. I'll revise those patches.
Philipp Schlehuber (d9ae38d1) at 27 Mar 11:51
Introduce new ways to split an automaton
... and 2 more commits
I fixed some typos in the man pages with a particular focus on spot-x
.
However, there is still a problem with HTML generation as can be seen here: https://spot-dev.lre.epita.fr/man/spot-x.7.html .
Locally (i.e. localhost), I could confirm that the man pages generated are fine, but the HTML is not.
I can't figure why the BIBLIOGRAPHY is rendered as this big bold blob.
Also, I did not find what are the rules about hyphens in options (e.g. --verbose
) or the use of Unicode characters (e.g. Büchi).
Pierre Ganty (2dfbe191) at 27 Mar 10:27
Small fixes in the man pages
Pierre Ganty (88f8af22) at 27 Mar 10:24
Philipp Schlehuber (24231f50) at 27 Mar 08:51
Introduce new ways to split an automaton
Philipp Schlehuber (349bf1cc) at 27 Mar 08:04
Introduce new ways to split an automaton
... and 20 more commits
Alexandre Duret-Lutz (6136b789) at 26 Mar 21:11
modernize some Python code
merged manually
The following are cases extracted from the same Pecan run mentioned in #566 and coming from an email from @pierreganty. On these automata, running autfilt --small
takes increasingly more time, because of simulation-based reductions.
postproc126.hoa.xz postproc144.hoa.xz postproc162.hoa.xz
% autfilt --small postproc1{26,44,62}.hoa --stats='%S->%s (%X APs, %r seconds)'
126->16 (16 APs, 4.2536 seconds)
144->18 (18 APs, 18.7157 seconds)
162->20 (20 APs, 140.485 seconds)
I have a couple of extra larger automata, but the files start to be very large and I don't think it is necessary to attach them here.
Running valgrind --tool=callgrind
on the smallest of these three shows the following profile
Beware that the time reported with %r
above do not take parsing into account, but the above profile does.
On the profile, we can see that 91.5% of the time is spent doing 4 simulation-based reductions (2 forward, 2 backward), and that 35% of the time is in merge_edges()
. I suspect we have a lot of edges to merge, because build_results
uses minterms_of
to iterate over the 2^AP possible labels. Surely this can be improved. Maybe we don't need to merge any edges between iterations of the simulation-based reductions: can we wait the end? Second, we should probably be able to replace the minterms_of
iteration by an iteration a label basis computed by the edge_separator
introduced for #566. Actually the label basis of the automaton was used to declare aliases in the HOA file to shorten it greatly: there are only 90 of them in this automaton, so that's really small compared to 2^16.