--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
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: 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. 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.