HI,
My name is Roei Nahum. Your wonderful platform helps me to translate temporal formulas into Buchi automata. I downloaded Spot (version 2.9.4), and wrote a C++ program based on Spot API.
As the following code snippet shows, I configured Spot so it will produce small state-based Buchi automata. I also skip the wdba minimalization.
spot::option_map extra_options; spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::translator* trans; extra_options.set("wdba-minimize", 0); trans = new spot::translator(dict, &extra_options); trans->set_type(spot::postprocessor::BA); trans->set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans->run(pf.f);
Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing:
(!G(!({{a ##[1:500] b} ##[1:500] c})))
Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged?
Thanks in advance, Roei
Roei Nahum roeina@nvidia.com writes:
Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing:
(!G(!({{a ##[1:500] b} ##[1:500] c})))
Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged?
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
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@lrde.epita.fr Sent: Sunday, November 14, 2021 3:19 PM To: Roei Nahum roeina@nvidia.com Cc: spot@lrde.epita.fr; Yael Meller yael@nvidia.com Subject: Re: Assistance with Spot
External email: Use caution opening links or attachments
Roei Nahum roeina@nvidia.com writes:
Spot works very well on few examples I checked, but having a hard time with the following formula, in which it runs for a very long time without finishing:
(!G(!({{a ##[1:500] b} ##[1:500] c})))
Can you please help me understand why? Is there anything I can configure differently in order to help it to be converged?
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
Roei Nahum roeina@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...
-
Alexandre Duret-Lutz -
Roei Nahum