Hi,
I'm using / comparing Spot and other tools in the Rabin to Parity
translation. I have two questions (to ensure my comparison is fair):
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
The last two are an effort to ensure that simplify-acc doesn't change
the acceptance condition.
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). Just to make sure: Are there other
DRA-to-DPA translations included in Spot which are worthwhile to be
investigated?
Cheers,
Tobias