formula where WDBA-minimization is both slow and unnecessary
This was reported by Roei Nahum.
Translating the following formula has a clear exponential runtime.
% for i in $(seq 1 20); do
ltl2tgba --small -B -f "(!(G({(a)} |=> {(b)[*$i]})))" --stats="i=$i: %s states, %rs";
done
i=1: 3 states, 0.000980134s
i=2: 4 states, 0.00161671s
i=3: 5 states, 0.00199145s
i=4: 6 states, 0.00283387s
i=5: 7 states, 0.00336581s
i=6: 8 states, 0.00495071s
i=7: 9 states, 0.00683196s
i=8: 10 states, 0.0120013s
i=9: 11 states, 0.00975352s
i=10: 12 states, 0.0136751s
i=11: 13 states, 0.0231716s
i=12: 14 states, 0.0372669s
i=13: 15 states, 0.0729032s
i=14: 16 states, 0.153856s
i=15: 17 states, 0.299823s
i=16: 18 states, 0.656352s
i=17: 19 states, 1.48609s
i=18: 20 states, 3.0405s
i=19: 21 states, 6.51409s
i=20: 22 states, 13.3897s
That's caused by WDBA-minimization:
% for i in $(seq 20 32); do
ltl2tgba --small -B -x '!wdba-minimize' -f "(!(G({(a)} |=> {(b)[*$i]})))" --stats="i=$i: %s states, %rs";
done
i=20: 22 states, 0.0161525s
i=21: 23 states, 0.0130079s
i=22: 24 states, 0.0135806s
i=23: 25 states, 0.013995s
i=24: 26 states, 0.0147525s
i=25: 27 states, 0.0159907s
i=26: 28 states, 0.0169671s
i=27: 29 states, 0.0182638s
i=28: 30 states, 0.0224162s
i=29: 31 states, 0.0198878s
i=30: 32 states, 0.0216118s
i=31: 33 states, 0.0222848s
i=32: 34 states, 0.0233845s
However I thought that the point of 69c82115 was to avoid exactly this problem by canceling WDBA-minimization when it creates too many states? Something must be wrong.