HI,
My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I'm having an issue and I'll appreciate if you can assist.
I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API. The program I wrote is basically like this:
...get the formula... spot::parsed_formula cex_pf = spot::parse_infix_psl(formula); if(cex_pf.format_errors(std::cerr)){ cout << "Invalid formula syntax: " << formula << endl; exit(1) } spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans.run(cex_pf.f); ...print the automata...
I tried running this code on several formulas, and it works great.
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?
Thanks, Roei Nahum
A small fix: the problematic formula is:
(!(G({(a)} |=> {(b)[*32]})))
From: Roei Nahum Sent: Tuesday, December 8, 2020 2:33 AM To: spot@lrde.epita.fr Subject: Spot question
HI,
My name is Roei Nahum. I recently got to know SPOT, and first of all, I want to thank you for this great platform. I'm having an issue and I'll appreciate if you can assist.
I use SPOT in order to translate temporal formulas into automata. To do so, I downloaded spot, and wrote a C++ program based on SPOT API.
The program I wrote is basically like this:
...get the formula... spot::parsed_formula cex_pf = spot::parse_infix_psl(formula); if(cex_pf.format_errors(std::cerr)){ cout << "Invalid formula syntax: " << formula << endl; exit(1) } spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); twa_graph_ptr aut = trans.run(cex_pf.f); ...print the automata...
I tried running this code on several formulas, and it works great.
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?
Thanks, Roei Nahum
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 -
Roei Nahum