study effect of degen-lcache on ba-simul
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 511
enabling lcache
causes some transitions to be merged
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=0 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
68 4272 499
but it hinders the BA simulation-based reductions
% ltl2tgba --ba -x degen-lcache=1,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2032 183
% ltl2tgba --ba -x degen-lcache=0,degen-reset=1,ba-simul=1 '(GFa -> GFb) & (GFc -> GFd) & GF(Fe & X(f | X!f))' --stats '%s %t %e'
45 2016 187
This suggest that either we could fine-tune degen-lcache
to pick a
more suitable level when offered the choice (maybe take the "natural"
level when offered the choice), or we could devise a simulation-based
reduction that is tailored to degeneralized automata (where we know
that cloned states recognized the same languages).