Hi Tobias ! Tobias Meggendorfer <tobias.meggendorfer@ist.ac.at> writes:
1) I want to minimize the input automata using Spot to remove the effects of preprocessing done by each tool as much as possible. However, I require that the acceptance condition remains a Rabin condition. Right now, I am using the call
autfilt --remove-dead-states --cleanup-acceptance --remove-unused-ap --simplify-exclusive-ap --simplify-acc --partial-degeneralize --generalized-rabin --deterministic
--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. --simplify-acc already implies --cleanup-acceptance, and will simplify the formula of the acceptance conditions as it can, but it cannot be restricted to produce a specific type of output. This is really meant as a preprocessing for algorithms that works on arbitrary acceptance. The order in which you list the options does not influence the order in which autfilt executes their algorithms. Generally if you want to be sure that some algorithm is executed before another one, you need to call autfilt multiple times, or check the order in the code (yes, this is not very nice). Here the order of execution is 1. simplify acceptance condition 2. remove dead states 3. partial degeneralize 4. postprocess automaton (with type --generic [by default], preference --deterministic, and level --high [default once --deterministic is given]) 5. convert to generalized_rabin 6. remove unused AP --generalized-rabin is (unfortunately) an algorithm and not a simplification constraint for the postprocessor (which is a piece of spaghetti code normally in share of deciding what algorithm should be run to convert and simplify an automaton into the desired type, so you don't have to find that by yourself). So far Spot's postprocessor does not know how to output Rabin or Generalized Rabin output. removing dead states and simplifying the acceptance conditions is already done by the postprocessor, so I don't think you need to run those first. I believe removing AP is done as well (I remember we recently fixed one scenario where that was unexpectedly not done, but I don't think it was on the --generic path).
The last two are an effort to ensure that simplify-acc doesn't change the acceptance condition.
If the input is Rabin, I do not think that simplify-acceptance can currently do much more than producing what we call Rabin-like (i.e. Rabin with some pairs simplified to a single Inf or Fin). So just running generalized-Rabin on the output of the postprocessor should be enough to get add any missing Fin (you may still have generalized pairs without Inf) autfilt --deterministic --generalized-rabin The only case I can think where using partial-degeneralize would help is if you have for instance (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)) where Inf(1) and Inf(3) are always satisfied by the automaton. Then simplify-acc will output Fin(0) | Fin(2) | (Fin(4) & Inf(5)) and partial-degeneralization would enlarge the automaton to produce a final formula like Fin(0) | (Fin(1) & Inf(2)). 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...
2) What are the ways to tell spot to translate DRA to DPA? Right now, I am using autfilt --hoa --deterministic --parity. This seems to be a sort of black box (which is fine with me).
Yes, this goes through the aforementioned postprocessor, which is in charge of deciding how to determinize and convert the input to parity. No determinization to be done here, luckily. Paritization is done via the monster procedure presented in our ATVA'20 paper, but in the case of DRA input it mostly reduces to your LCS'17 paper, modulo a few differences: - the above acceptance simplifications are done on each component (not only at the automaton level), - we use some heuristics for ordering the move of multiple colors at once in a record, - and we propagate the colors of edges to their neighboring edges when it is guaranteed to be equivalent (if all outgoing edges (non-self-loop) of a state share some colors, those colors can be added to all incoming edges (non-self-loops), and vice-versa). 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.
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. The guy to talk to if you need more details about to_parity() is Florian Renkin, in Cc:. Alexandre