- Spot - LRE

Converting LTL_f to a finite automaton and plotting it via Graphviz.
by Bhatia, Amit RTX 15 Oct '21

15 Oct '21

Hello Spot Team, I recently came across your tool while searching for existing implementations to convert an LTL formula with finite semantics into a finite automata together with rendering it pictorially (e.g., using graphviz tool) - I was wondering if you have any examples of how this could be accomplished when the end goal is also to plot the automaton using GraphViz? I did read through https://spot.lrde.epita.fr/tut11.html (Translating an LTL formula into a monitor) and https://spot.lrde.epita.fr/tut12.html (Working with LTL formulas with finite semantics), but I am not sure if the output is already compliant with Graphviz's required format or some parsing is required (my knowledge of Graphviz is also fairly limited). Thanks, Amit Amit Bhatia Raytheon Technologies Research Center Berkeley, CA Amit.Bhatia2(a)rtx.com<mailto:Amit.Bhatia2@rtx.com>

2 1

Re: [Spot] Spot question
by Roei Nahum 05 Oct '21

05 Oct '21

Hi, Following the attached thread from December 2020. When working with version 2.9.4 of Spot, I got an endless runtime when I tried to create a small BA of this formula: (!(G({(a)} |=> {(b)[*32]}))) Thanks to your help, I understood that there was a bug in the mechanism that should avoid the WDBA-minimization in cases it creates to much additional states. (alexandre opened an issue for me – https://gitlab.lrde.epita.fr/spot/spot/-/issues/443) Was this bug fixed in any of the later versions? I met some additional problematic formulas. Currently, my only option to process such formulas is to avoid the WDBA-minimization step. Thanks in advance, Roei ******************* -----Original Message----- From: Roei Nahum Sent: Tuesday, December 8, 2020 5:40 PM To: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Subject: RE: [Spot] Spot question Great, now I get it. Thanks for the clarifications and debugging. I appreciate the time you spent to help. Roei ******************* -----Original Message----- From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> Sent: Tuesday, December 8, 2020 3:13 PM To: Roei Nahum <roeina(a)nvidia.com> Subject: Re: [Spot] Spot question External email: Use caution opening links or attachments On Tue, Dec 8, 2020 at 12:32 PM Roei Nahum <roeina(a)nvidia.com> wrote: > > Thanks Alexandre! I really appreciate your help. > > Disabling WDBA-minimize indeed fixed the problem. > > I have few questions, for better understanding. > > (1) What is the WDBA-minimize optimization and what it is used for? > Is it just a way to try minimizing the size of the produced automata? > Will I get a state-based Buchi automata even if I'll disable this optimization? A subset of LTL formulas, representing what are known as "obligation properties", can be translated into Weak Deterministic Büchi Automata. Those WDBA can be minimized using techniques similar to DFA minimization, i.e. in O(n log n), while minimization of DBA in general is NP-complete. So whenever you translate an LTL formula with an optimization level set to High (the default), and even if you do not specifically asked for a deterministic automaton, the translator will try to determinize your automaton and check if it is a WDBA to minimize it. Quite often, the minimal WDBA obtained is smaller than the non-deterministic BA that we were able to construct otherwise. See https://nam11.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.lrde.ep… for a high-level view of the LTL translation pipeline. And references to the WDBA papers. Using "!wdba-minimize" is simply disabling the bottom branch, but you still get some simulation-based reductions in the top branch. A quite dated benchmark from around the time when WDBA minimization was introduced in Spot shows the effect of activating it: https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.lrde.… (The option names at the bottom of the first page are unrelated to those used today.) I consider this option to be the most useful automaton simplification in Spot, and the reason why automata produced by Spot are often smaller than those of other tools. (Hence the reason why I called this the "secret weapon" of Spot in the aforementioned slides.) The main problem with WDBA is that it requires a determinization. In the case of !G({a} |=> {b[*32]}), which can also be written as F(a & F[1:32]!b), there is a non-deterministic choice on the first state (see attachment). The determinization (a simple powerset construction) creates an exponential number of states, before the minimization has a chance to reduce it to 34 states. In fact for this particular kind of automata (with a "terminal" accepting state), I believe I should be able to write a smarter determinization that would keep 34 states in this very case. > (2) What do you mean by saying "I can still reproduce it."? > I'm working with version 2.9.4 of spot. Is there a more updated version where the problem is fixed? Or do you talk about future release? The 2.9.x versions are just bug fixes above version 2.9 released in April. The latest is 2.9.5, but if 2.9.4 works for you, there is no serious reason to upgrade. On the development version of Spot, which will probably be released as 2.10 early next year, I have made some changes meant to abort some determinization-based algorithms when they are optional and take too long. In the case of WDBA-minimization, the determinization is now meant to be aborted whenever it would create more than 4096 additional states. But you just highlighted a bug in that implementation. With the fix, I now see this: % for i in $(seq 1 32); do ./ltl2tgba "F(a & F[1:$i]\!b)" --stats="i=$i: %s states, %rs, det=%d"; done i=1: 3 states, 0.00108319s, det=1 i=2: 4 states, 0.00154409s, det=1 i=3: 5 states, 0.00198193s, det=1 i=4: 6 states, 0.00286866s, det=1 i=5: 7 states, 0.00366207s, det=1 i=6: 8 states, 0.00516698s, det=1 i=7: 9 states, 0.00783739s, det=1 i=8: 10 states, 0.0136073s, det=1 i=9: 11 states, 0.0108086s, det=0 i=10: 12 states, 0.0147442s, det=0 i=11: 13 states, 0.0231776s, det=0 i=12: 14 states, 0.0161911s, det=0 i=13: 15 states, 0.0161992s, det=0 i=14: 16 states, 0.0164307s, det=0 i=15: 17 states, 0.017823s, det=0 i=16: 18 states, 0.0197592s, det=0 i=17: 19 states, 0.0197573s, det=0 i=18: 20 states, 0.0203755s, det=0 i=19: 21 states, 0.020358s, det=0 i=20: 22 states, 0.0218632s, det=0 i=21: 23 states, 0.0229568s, det=0 i=22: 24 states, 0.0234896s, det=0 i=23: 25 states, 0.0295049s, det=0 i=24: 26 states, 0.0254808s, det=0 i=25: 27 states, 0.0256344s, det=0 i=26: 28 states, 0.0266605s, det=0 i=27: 29 states, 0.028628s, det=0 i=28: 30 states, 0.0296059s, det=0 i=29: 31 states, 0.0304871s, det=0 i=30: 32 states, 0.0319202s, det=0 i=31: 33 states, 0.0332124s, det=0 i=32: 34 states, 0.0340735s, det=0 See how the translation stopped building deterministic automata at i=9. Without WDBA-minimization you'd get non-deterministic automata everywhere. If my plan for a better determinization for terminal automata works I hope to get deterministic automata on all those lines. -- Alexandre Duret-Lutz External email: Use caution opening links or attachments ******************* On Tue, Dec 8, 2020 at 8:07 AM Roei Nahum <roeina(a)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://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.lr… -- Alexandre Duret-Lutz ******************* 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

2 1

Unambiguous refinements of collections of BDDs
by Michaël Cadilhac 02 Aug '21

02 Aug '21

Hi there all, Since I started using BDDs in automata, I have faced the following computational problem a few times. If you have any insight on how to solve it more efficiently, I'd be very interested. In particular, is there a spot in spot where this is implemented? Let me spell the problem out in general terms, then tie it to BDDs. *Definitions.* - A collection C of sets over a finite universe U is *unambiguous* if all sets in C are pairwise disjoint. In other words, C is a partition of the union of its sets. - A collection C' refines a collection C if each set in C can be obtained as the union of sets in C'. *Problem.* Given a collection C, compute a (minimal) unambiguous refinement of C. [[For complexity purposes, the computational task can also be written as: Given C and k, does there exist an unambiguous refinement of C of size < k? This is certainly NP-complete ([SP7] in Garey and Johnson is that problem without "unambiguous").]] *Motivation.* In BDDs, my use case is to have C be a collection of BDDs and a BDD represent the set of its satisfying assignments. Building an unambiguous refinement of BDDs seems an essential step in determinization: If I have a state with two outgoing transitions labeled with BDDs {F, G} such that F&G is not False, then this state is nondeterministic. To determinize it, we will have to consider the transition labels {F&G, F&!G, !F&G}. Note that this set refines {F, G}, since F = (F&G)|(F&!G) and similarly for G. *Question.* What is known about that problem? Is there a good heuristic for it that would give an unambiguous refinement not far from the optimal? *Implementations.* I implemented it in a few different ways and would be interested in alternative implementations. Two options I have are: *- The straightforward way:* 1. C' = {U} (recall that U is our universe, with BDDs this would be True) 2. for each S in C: 3. for each S' in C': 4. if (S cap S' is not empty) 5. Remove S' from C' 6. Add (S cap S') and (S^c cap S') to C' (^c denotes complement). *- A slightly more complex implementation.* I encode C' as a BDD itself, introducing lots of fresh variables; namely, if C' = {F, G} for two BDDs F and G, I introduce two fresh variables X_F and X_G, and encode C' as (F & X_F) | (G & X_G). This allows lines 3 and 4 to become: 3. Compute C' & S and project it on the X_? variables. 4. Iterate through each of the variables that appear: if X_S' appears, this means that S cap S' is nonempty. Thanks for reading! Cheers, Michaël

2 1

Time to decide inclusion
by Pierre Ganty 02 Aug '21

02 Aug '21

Dear Spot devs, I want to measure how much time it takes Spot to decide whether the language of the automaton A is contained in that of B. I've been using the following command ``` autfilt '--stats=%r, %R' A.hoa --included-in=B.hoa ``` I think I am not interpreting the results correctly because `--stats` reports very small numbers while adding `time` in front of the command reports much much larger numbers (several orders of magnitude larger). What's the right way to measure the time it takes Spot to decide the inclusion? Thank you. Pierre.

2 1

latexmk required to build spot
by Maxime Bouton 29 May '21

29 May '21

Dear spot maintainers, I am trying to compile spot v2.9.7 from source but my build errors due to latexmk not being available in the environment. From what I understand from the log, it is used in making the doc, is there a way to skip this step in the build? I built it on ubuntu (gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0) and it did not complain about latexmk, this only happened when changing to a new platform (the end goal is to cross compile it). Any help would be appreciated, Maxime I am using a linux platform with gcc: x86_64-linux-gnu-g++ (GCC) 9.1.0 Here is what I run: ./configure --prefix=${prefix}/spot-build --build=${MACHTYPE} --host=${target} --disable-python make -j${nproc} && make install Here is the partial log: ``` [15:46:03] Making all in doc [15:46:03] make[2]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] Making all in tl [15:46:03] make[3]: Entering directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] BIBINPUTS='./..' latexmk -pdf -ps- -dvi- -pvc- -e '$bibtex_use=2' -e '$pdflatex="pdflatex %O \"\\def\\SpotVersion{2.9.7}\\input{%S}\""' ./tl.tex [15:46:03] /bin/sh: latexmk: not found [15:46:03] make[3]: *** [Makefile:1399: tl.pdf] Error 127 [15:46:03] make[3]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc/tl' [15:46:03] make[2]: *** [Makefile:1319: all-recursive] Error 1 [15:46:03] make[2]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7/doc' [15:46:03] make[1]: *** [Makefile:1341: all-recursive] Error 1 [15:46:03] make[1]: Leaving directory '/workspace/srcdir/jlspot/spot-2.9.7' ````

2 2

[Not-really-Spot] BDD libraries
by Michaël Cadilhac 27 May '21

27 May '21

Hi there ADL & all, Apologies for the not-really-spot question, but the expertise on this list is quite unique! I'm about to embark on a new project that relies on BDD. My only experience with BDD libraries was through using Spot, so I'm familiar with BuDDy, but that's it. Starting something fresh, I'm pondering what's the best C++ BDD library available nowadays. I axed through BuDDy and refactored it so that it's template-only and encapsulated the global variables in a class (hoping for some performance boost from inlining). While I'm fairly happy with the result, I now realize that there's been some progress in the BDD landscape since 1997—crazy! This paper: https://www.tvandijk.nl/pdf/2015setta.pdf by the author of Sylvan seems to indicate that Sylvan offers good performances on a single core, and great perf on multicore. It also comes with a nice C++ interface. I guess my question is: If you had to go from scratch today, which BDD library would you use? Cheers, M.

2 3

Walking through BDD formula in python
by Ayrat Khalimov 26 May '21

26 May '21

hi! With the aid of SPOT I am developing a counter-example guided synthesizer in python. See [1] if interested for details. My question is: I am trying to parse twa_run in python, namely, parse the labels of the each step (`spot.impl.step`). Is there a python way to walk through BDD? (The label is a simple cube expressed in BDD, and I need to convert it into my internal structure) (yes, this is rather a question about python interface for buddy) (no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial) [1] The idea is - guess the model, - then model check it and get a counter-example - then encode the counter-example into the "guesser" (which uses an SMT solver) thanks, Ayrat

2 5

fail to install spot
by Jueming Hu 15 Apr '21

15 Apr '21

Good afternoon, I am Jueming, a Ph. D. student at Arizona State University. I would like to use spot for my research, such as getting the graph of an LTL formula. I downloaded 'linux-64/spot-2.9.6-py38_2.tar.bz2' and ran 'conda install -c adl spot' within the extracted folder. 'spot 2.5.2' is shown in conda list and also in python packages. However, 'import spot' doesn't work. The error says, 'No module named 'spot''. I have also tried 'linux-64/spot-2.9.4-py38_2.tar.bz2', 'conda install -c adl/label/adl spot', 'conda install -c adl/label/dev spot', append system path before import spot, and export LD_LIBRARY_PATH. But spot still doesn't work on my pc. Could you please help me install spot? Thanks in advance and looking forward to hearing from you. Best, Jueming

2 1

Question about Transfoming from Non-deterministic Automata to Deterministic Automata
by Meng Ruijie 23 Mar '21

23 Mar '21

Dear Spot Team, Thanks for providing a wonderful tool. During constructing Buchi automata for LTL, Spot always shows non-determinism automata although I select the "deterministic" item. Would you mind telling me how to construct deterministic automata with Spot? Here is one LTL: !(false R (iusr2_ai3_re13 & (! X (true U iusr2_ai3_re14) | X (true U (iusr2_ai3_re14 & (true U ousr2_ai3_ce8)))))). The following is its automata but non-determinism. [cid:83ad2cd0-bc60-443c-b387-4bc7953c05d2] Looking forward to your response. Kind Regards, Ruijie

2 1

Translations to DPA
by Tobias Meggendorfer 18 Mar '21

18 Mar '21

Hi, I'm using / comparing Spot and other tools in the Rabin to Parity translation. I have two questions (to ensure my comparison is fair): 1) I want to minimize the input automata using Spot to remove the effects of preprocessing done by each tool as much as possible. However, I require that the acceptance condition remains a Rabin condition. Right now, I am using the call autfilt --remove-dead-states --cleanup-acceptance --remove-unused-ap --simplify-exclusive-ap --simplify-acc --partial-degeneralize --generalized-rabin --deterministic The last two are an effort to ensure that simplify-acc doesn't change the acceptance condition. 2) What are the ways to tell spot to translate DRA to DPA? Right now, I am using autfilt --hoa --deterministic --parity. This seems to be a sort of black box (which is fine with me). Just to make sure: Are there other DRA-to-DPA translations included in Spot which are worthwhile to be investigated? Cheers, Tobias

2 3