On Tue, Dec 8, 2020 at 8:07 AM Roei Nahum <roeina@nvidia.com> wrote:
The problems started when I processed this formula:
!G({(a)} |=> {(b)[*32]})
The code is running for a long time (more than a hour) without giving a result.
Did it get stuck? Is there any way I can make it work?
Humm, this formula seems to be taking an exponential time to translate: % 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 Passing --low (that's "trans.set_level(spot::postprocessor::Low);" for you) to remove all simplifications seems to produce automata of equivalent size much faster: % for i in $(seq 16 32); do ltl2tgba --small -B --low -f "(!(G({(a)} |=> {(b)[*$i]})))" --stats="i=$i: %s states, %rs"; done i=16: 18 states, 0.0013444s i=17: 19 states, 0.00170704s i=18: 20 states, 0.00172487s i=19: 21 states, 0.00159999s i=20: 22 states, 0.00181502s i=21: 23 states, 0.00237525s i=22: 24 states, 0.00208415s i=23: 25 states, 0.00253886s i=24: 26 states, 0.00216258s i=25: 27 states, 0.00239979s i=26: 28 states, 0.00271767s i=27: 29 states, 0.0025924s i=28: 30 states, 0.00297612s i=29: 31 states, 0.00285316s i=30: 32 states, 0.00323873s i=31: 33 states, 0.00352748s i=32: 34 states, 0.00316449s Alternatively, it's possible to keep all simplifications on, but just disable WDBA-minimization with % ltl2tgba --small -B -x '!wdba-minimize' -f "(!(G({(a)} |=> {(b)[*32]})))" --stats="%s states, %rs" 34 states, 0.0236776s To do the above in C++, you need to create and option_map object and pass it to the translator object, as in : ... spot::option_map extra_options; extra_options.set("wdba-minimize", 0); spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::translator trans(dict, &extra_options); ... I'll look more into it, because I thought I had fixed that problem in the development version of Spot a couple of months ago, but I can still reproduce it. I'll post updates on https://gitlab.lrde.epita.fr/spot/spot/-/issues/443 -- Alexandre Duret-Lutz