case where autfilt --small --high -B inputs a BA and produce a larger one
The input is a BA with 19 states:
% ltlfilt -s -f '!(((p1 W c1) U Gp2) || (GXc2 <-> F!F!c1))' | ltl3ba -M0 -F - > never
% autfilt --stats=%s never
19
Simplifications produce a TBA with 18 states:
% autfilt --exclusive-ap=c1,c2 --high --small --stats=%s never
18
But if we ask for a BA, we get a larger number of states:
% autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s never
20
We never want more states than the input in this case. This suggests at least two fixes
- The additional two states are introduced when the 18 state TBA is degeneralized into a BA. The degeneralization could probably be taught a trick to save at least one state here. (This requires some investigation.)
- When
postproc
inputs a BA and the desired output is also a BA, we should skip the transition-based simulation reductions, and use only the BA version of the simulation.