- Spot - LRE

ltlsynt and hoa input
by Ayrat Khalimov 06 Jan '22

06 Jan '22

hello, Is there a way to feed HOA file (as a nondet Buchi) instead of a formula to ltlsynt? I tried smth (see below), but I am getting 'unrealisable' for nondet Buchi automaton spec that is supposed to be realisable (see attached). Maybe I missing something? (like ltlsynt dualising the automaton, etc.) Here is what I tried. Into file synthesis.cc, add: #include "spot/parseaut/public.hh" Then in line 822, comment out: // auto aut = trans.run(f); and instead add: spot::bdd_dict_ptr dict = spot::make_bdd_dict(); auto parsed_aut = parse_aut("/tmp/spec.hoa", dict); if (parsed_aut->aborted) abort(); auto aut = parsed_aut->aut; This forces ltlsynt to read file "/tmp/spec.hoa" and ignore the formula. Further, when calling ltlsynt, pass the argument --decompose=no ('just in case'): ./ltlsynt --formula="GF a" --ins=x,y --dot --outs=a,b,c --decompose=no and provide the correct --ins and --outs arguments, and any formula with one of those propositions. The tool outputs expected implementations on toy examples, but on a larger example attached it outputs "unrealizable" instead of "realizable". That is why the question. best wishes, Ayrat

2 5

Spot Debian package not working due to expired certificate error for the LRDE website
by Young, David Clark 02 Jan '22

02 Jan '22

Hi, I am trying to install Spot using the Debian package at www.lrde.epita.fr/repo/debian/ but it looks as though the security certificate for www.lrde.epita.fr has expired. In fact, it looks like it expired yesterday (Dec. 29th). The reason I'm installing Spot is that it's a dependency of another project I would like to install, and that project's Dockerfile uses the Debian package. It is possible to compile Spot from the source, but it is more efficient to use a Debian package (and potentially eases reproducibility, which is nice when using Docker). Would it be possible for someone to update the certificate? Thanks! - David

2 1

SPOT: formula:is_literal shall be marked const?
by Ayrat Khalimov 02 Dec '21

02 Dec '21

hi Alexandre, Seems like the function formula::is_literal() should be marked const: /// \brief Whether the formula is an atomic proposition or its /// negation. bool is_literal() { return (is(op::ap) || // If f is in nenoform, Not can only occur in front of // an atomic proposition. So this way we do not have // to check the type of the child. (is(op::Not) && is_boolean() && is_in_nenoform())); } kind wishes, Ayrat

2 1

[BUG] Tests fail to build on FreeBSD: error: use of undeclared identifier 'sched_getcpu'
by Yuri 23 Nov '21

23 Nov '21

On FreeBSD 13 version 2.10 fails to build tests: c++ -DHAVE_CONFIG_H -I. -I.. -I.. -I.. -I../buddy/src \-I../lib -I../lib -fno-omit-frame-pointer -D_THREAD_SAFE -DNDEBUG -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -pthread -O2 -pipe -fno-omit-frame-pointer -fstack-protector-strong -fno-strict-aliasing -fno-omit-frame-pointer -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++17 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT ltsmin/modelcheck-modelcheck.o -MD -MP -MF ltsmin/.deps/modelcheck-modelcheck.Tpo -c -o ltsmin/modelcheck-modelcheck.o `test -f 'ltsmin/modelcheck.cc' || echo './'`ltsmin/modelcheck.cc In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:122:43: error: use of undeclared identifier 'sched_getcpu' << ": on CPU " << sched_getcpu() << '\n'; ^ ../spot/mc/mc_instanciator.hh:134:9: error: unknown type name 'cpu_set_t'; did you mean 'cpusetid_t'? cpu_set_t cpuset; ^~~~~~~~~ cpusetid_t /usr/include/sys/types.h:86:22: note: 'cpusetid_t' declared here typedef __cpusetid_t cpusetid_t; ^ In file included from ltsmin/modelcheck.cc:27: ../spot/mc/mc_instanciator.hh:135:9: error: use of undeclared identifier 'CPU_ZERO' CPU_ZERO(&cpuset); ^ ../spot/mc/mc_instanciator.hh:136:9: error: use of undeclared identifier 'CPU_SET' CPU_SET(i, &cpuset); ^ ../spot/mc/mc_instanciator.hh:137:18: error: use of undeclared identifier 'pthread_setaffinity_np' int rc = pthread_setaffinity_np(threads[i].native_handle(), ^ ../spot/mc/mc_instanciator.hh:138:48: error: use of undeclared identifier 'cpu_set_t' sizeof(cpu_set_t), &cpuset); ^ 6 errors generated. Thanks, Yuri

2 1

Re: [Spot] Assistance with Spot
by Alexandre Duret-Lutz 19 Nov '21

19 Nov '21

Roei Nahum <roeina(a)nvidia.com> writes: > I didn’t fully understand what utility I miss by lowering tls-impl to > 2 (or to lower values) - are there additional materials I can use? Implication-based simplifications of LTL formulas are described in section 5.4.3 of https://spot.lrde.epita.fr/tl.pdf tls-impl=1 corresponds to tl_simplifier_options::synt_impl tls-impl=2 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks tls-impl=3 corresponds to tl_simplifier_options::synt_impl + tl_simplifier_options::containment_checks + tl_simplifier_options::containment_checks_stronger One question is whether your formulas require such simplification at all.

2 4

Behavior change in autfilt from 2.9.7 to 2.10
by Pierre Ganty 17 Nov '21

17 Nov '21

Hi, When invoking `autfilt sub.aut --included-in=sup.aut` on the two enclosed Buchi automata with Spot 2.10 I am getting: ``` Too many acceptance sets used. The limit is 32. ``` With Spot 2.9.7 I was getting a non-terminating execution. Is it the expected result? If so, what is the explanation behind the too many acceptance sets? Is it the complementation procedure for `sup.aut` that fails? Thank you and keep up with the excellent work, Pierre.

2 1

Evaluating a word on an automaton/formula
by Fatma Faruq 17 Nov '21

17 Nov '21

Hi, I was wondering if someone could point me to resources in spot that show how to evaluate an LTL word or trace on an automaton. Or anyway to check whether a trace or word satisfies a particular LTL formula. I'm new to Spot. So far I've been able to use the python notebook - word, (and other examples) to iterate over an automaton generated from an LTL formula. Thank you so much, -- Regards, Fatma

2 1

Assistance with Spot
by Roei Nahum 16 Nov '21

16 Nov '21

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

2 3

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