16 Nov
2021
16 Nov
'21
3:24 p.m.
Roei Nahum <roeina(a)nvidia.com> writes:
Thanks Alexandre!
I get a similar problem with this formula:
(F(({("a1") ##[1:$i] ("a2") ##[1:$i] ("a3")}!)))
This formula doesn't suffer from explosion of states in the produced automata.
For:
i = 10 --> 22 states
i = 11 -> 24 states
and in general --> number of states = (i * 2) + 2
However, my run still get stuck when I try to set higher value for i (such as 30).
Is it because the non-determinism introduced by ##[1:i]? Is there something to do about
it?
With --low optimizations, I'm able to translate larger values:
% for i in 50 100 150 200 250; do
ltl2tgba-2.9.6 --low \
--stats="i=$i %s states, %e edges, %r seconds" \
"F{a1 ##[1:$i] a2 ##[1:$i] a3}\!"
done
i=50 102 states, 201 edges, 0.0311227 seconds
i=100 202 states, 401 edges, 0.504395 seconds
i=150 302 states, 601 edges, 2.44754 seconds
i=200 402 states, 801 edges, 6.80465 seconds
i=250 502 states, 1001 edges, 18.3883 seconds
Adding -x simul=0 to disable simulation-based
reductions is much faster
% for i in 50 100 150 200 250; do
ltl2tgba-2.9.6 --low -x simul=0 \
--stats="i=$i %s states, %e edges, %r seconds" \
"F{a1 ##[1:$i] a2 ##[1:$i] a3}\!"
done
i=50 102 states, 201 edges, 0.00202422 seconds
i=100 202 states, 401 edges, 0.0109756 seconds
i=150 302 states, 601 edges, 0.011566 seconds
i=200 402 states, 801 edges, 0.0156098 seconds
i=250 502 states, 1001 edges, 0.0257548 seconds
Note that I've discovered something really embarrassing while playing
with this parametric formula: the bounds of ##[a:b] are stored in 8 bits
variables, and to make things worse, nothing is checking for overflow...
https://gitlab.lrde.epita.fr/spot/spot/-/issues/485