18 Mar
2021
18 Mar
'21
1:35 p.m.
Hi Alexandre,
thank you for the detailed answer, this helps me a lot :-) Some replies
below (not sure if this still belongs on the mailing list, feel free to
block it :-) )
On 18.03.2021 13:11, Alexandre Duret-Lutz wrote:
Thanks, but I think this is sufficient then. I only want to compare to
state-of-the-art :-) If "autfilt --parity --deterministic" gives the
"best" dra-to-dpa translation Spot can offer, this is exactly what I need.
--simplify-exclusive-ap does not make sense without
specifying exclusive
APs with --exclusive-ap, but it's unlikely that it makes sense in your
case. Here it has no effect.
Oops. I basically just threw whatever switch looked
like "simplify" on
there :-)
It's unclear if this partial-degeneralization can
be presented as a
"simplification" since the result has more states. When we did the
benchmark for our ATVA'20 paper, we found that was generally better, but
that there were a few cases that were better paritized without partial
degeneralization. Anyway, if you always prefer a smaller number of
Rabin pairs even at the cost of more states, it makes sense to use:
autfilt --cleanup-acceptance --partial-degeneralize \
--deterministic --generalized-rabin
I don't think you need more options. Eventually one might hope that we
teach the postprocessor how to produce Rabin/generalizedRabin, so that
users do not have to find what need to be executed before and after,
but even if it did, it's still unclear if the goal should be
to minimize the number of states or the number of pairs...
I see, thanks. Since the
number of pairs influences worst-case
exponentially I think it is fair to use this as pre-processing. I'm
working with randomly generated automata which might have extremely
stupid structures and I just want to ensure that the most obvious things
are removed, so that tools that don't figure out these obvious things
don't get an inherent disadvantage. Since all tools start from the same
data-set it doesn't matter that much if the number of states is blown up
a bit :)
Because this goes through the postprocessor, it will
also be slowed down
by some clostly simplifications that are later attempted on the DPA.
You can disable those with '-x wdba-minimize=0,simul=0' if you prefer.
Oh
great! I want to compare the constructions both with and without
"more advanced, generic" post-processing options, this is probably
exactly the switch I am looking for. Arguably "more advanced, generic"
is quite vague, basically I want to make Spot run only that dra-to-dpa
construction without too much fuzz around it, since Spot is just so damn
good at optimizing the automata that comparison to not-so-well-optimized
tools are always a bit tricky =). Of course, passing all generated
automata through the post-processor of Spot is an option, too, but I
prefer to have both comparisons (then we also see how much potential for
optimization other constructions have).
Btw, how does the "-x ..." switch compare to "--low"? Adding
"--low" to
"--parity --deterministic" does not seem to change much.
Just to make
sure: Are there other DRA-to-DPA translations included in
Spot which are worthwhile to be investigated?
That's the only implementation we have, but you also have to option to
write a small Python script or C++ program that calls the to_parity()
function in case you want to test it in isolation, or play with its
options.