a case when -G -D produce a parity automaton more than twice smaller than -P -D
The following formula comes from https://www.ruediger-ehlers.de/blog/deterministicparity.html
% f='!g & (GFr -> GFg) & FGinit & G(XXg -> (init & Xinit & XXinit)) & !Xg & G(!g | X!g) & G((init & !Xinit) -> (!r & !Xr))'
With Spot 2.8.5.dev
% ltl2tgba -G -D -f "$f" --stats="%s states, %[o]g"
5 states, parity min odd 3
% ltl2tgba -P -D -f "$f" --stats="%s states, %[o]g"
11 states, parity min odd 3
It's related to LTL-splitting:
% ltl2tgba -G -D -x ltl-split=0 -f "$f" --stats="%s states, %[o]g"
11 states, parity min odd 3
Once we remove the obligation terms of the formula, we can reduce the case to this:
% ltl2tgba -P -D "(GFr -> GFg) & FGinit" --stats=%s
4
% ltl2tgba -G -D "(GFr -> GFg) & FGinit" --stats=%s
1
% ltl2tgba -G -D -x ltl-split=0 "(GFr -> GFg) & FGinit" --stats=%s
4
It's seem it's just "luck" that the construction of the formula follows a "parity pattern" and leads to a parity acceptance with -G
. Can we detect those cases?