Re: [Spot] Assistance with Spot

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? Thanks, Roei -----Original Message----- From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Sent: Sunday, November 14, 2021 3:19 PM To: Roei Nahum <roeina(a)nvidia.com> Cc: spot(a)lrde.epita.fr; Yael Meller <yael(a)nvidia.com> Subject: Re: Assistance with Spot External email: Use caution opening links or attachments Roei Nahum <roeina(a)nvidia.com> writes: Hi Roei, ##[1:i] introduces a lot of non-determinism, and !{...} requires a deterministic automaton to complement it, so the construction is blowing up rapidly. Setting i=500 seems hopeless given the following trend: % for i in `seq 1 15`; do ltl2tgba -x wdba-minimize=0 --low -B \ "(\!G(\!({{a ##[1:$i] b} ##[1:$i] c})))" \ --stats="i=$i gives %s states in %r seconds" done i=1 gives 4 states in 0.000520668 seconds i=2 gives 7 states in 0.000590509 seconds i=3 gives 13 states in 0.0018721 seconds i=4 gives 25 states in 0.00321669 seconds i=5 gives 49 states in 0.00543848 seconds i=6 gives 97 states in 0.0105915 seconds i=7 gives 193 states in 0.0207409 seconds i=8 gives 385 states in 0.0410949 seconds i=9 gives 769 states in 0.113351 seconds i=10 gives 1537 states in 0.307374 seconds i=11 gives 3073 states in 1.10505 seconds i=12 gives 6145 states in 3.69696 seconds i=13 gives 12289 states in 10.1515 seconds i=14 gives 24577 states in 54.9003 seconds i=15 gives 49153 states in 310.364 seconds I do not know what could be done here. Alexandre