May 2019 - Spot

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

LTLf to NBAs: inconsistent results from code and command line
by Yong Li (李勇) 04 Jun '19

04 Jun '19

Dear Spot developers, I am Yong Li, a Phd student from Chinese Academy of Sciences. I am writing to you to ask an implementation question about the translation from LTLf to NBAs in Spot. currently if I use following command line: ltlfilt --from-ltlf -f "((G((P83) -> (X((P145)) | X(X((P145))) | X(X(X((P145)))) ))) -> ( G((P21) -> (X( (P118) | (P83)) | X(X( (P118) | (P83))) | X(X(X((P118) | (P83)))) )) & G( (P118) -> X(!(P118))) & G( (P83) -> X(!(P118) U (P145)))))" | ltl2tgba | autfilt --remove-ap=alive --small -B I was able to get a weak DBA with only 8 states. However, if I use following c++ code to do the same job: auto pf1 = spot::parse_infix_psl(argv[1]); if (pf1.format_errors(std::cerr)) { std::cerr << "error: " << argv[1] << std::endl; return -1; } // formula auto f1 = pf1.f; std::cout << f1 << std::endl; // translate to ltlf //auto ltlf = spot::from_ltlf(f1, "alive"); spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); trans.set_level(spot::postprocessor::High); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f)); spot::remove_ap rem; rem.add_ap("alive"); aut = rem.strip(aut); spot::postprocessor post; post.set_type(spot::postprocessor::BA); post.set_pref(spot::postprocessor::Small); // or ::Deterministic post.set_pref(spot::postprocessor::High); // or ::Deterministic aut = post.run(aut); I would get a DBA with 16 states, which has much more states than the one from the command line. The full source code is attached to this email. Could you tell me how I can change the code above so to get the same DBA from the command line? Thank you very much. BTW: I would like to appreciate the Spot tool which is a tool I would install on my every Ubuntu system. Yong

2 3

Docker pull
by Jiraphapa Jiravaraphan 03 Jun '19

03 Jun '19

Dear Spot team, I've tried to pull docker image using command "sudo docker pull registry.lrde.epita.fr/spot-sandbox", however, I got the following response: "Unable to find image 'registry.lrde.epita.fr/spot-sandbox:latest' locally docker: Error response from daemon: error parsing HTTP 403 response body: invalid character '<' looking for beginning of value: "<!DOCTYPE HTML PUBLIC \"-//IETF//DTD HTML 2.0//EN\">\n<html><head>\n<title>403 Forbidden</title>\n</head><body>\n<h1>Forbidden</h1>\n<p>You don't have permission to access /v2/spot-sandbox/manifests/latest\non this server.<br />\n</p>\n</body></html>\n". See 'docker run --help'." , any insight would be appreciated. Best regards, Jiraphapa J.

3 2

Re: [Spot] ltlsynt light
by Victor Khomenko 21 May '19

21 May '19

Dear Alexandre and Guillermo, We tried to link Spot statically - Alexandre's suggestion did not quite work for us, but Danil had worked out a different method, see below. Regards, Victor. ------------------------ Hi Victor, This looks much simpler than the way I figured out by try and error: https://workcraft.org/devel/backend/spot However the binaries are still dynamically linked after this: ~/spot/bin$ ldd ltl2tgba linux-vdso.so.1 => (0x00007fff6c9f8000) libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x00007fe09b967000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fe09b65e000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x00007fe09b446000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fe09b07c000) /lib64/ld-linux-x86-64.so.2 (0x00007fe09bcf3000) I think I will stick for what is working for us rather than trying to understand what goes wrong with these --disable-shared and --enable-static flags... Maybe we should share our experience with Guillermo and also let Spot team know about the issue? Cheers, Danil > -----Original Message----- > From: Spot <spot-bounces(a)lrde.epita.fr> On Behalf Of Alexandre Duret- > Lutz > Sent: Tuesday, May 21, 2019 9:06 AM > To: Guillermo Perez <gaperez64(a)gmail.com> > Cc: spot <spot(a)lrde.epita.fr>; Guillermo A. Pérez > <guillermoalberto.perez(a)uantwerpen.be> > Subject: Re: [Spot] ltlsynt light > > On Tue, May 21, 2019 at 9:47 AM Guillermo Perez <gaperez64(a)gmail.com> > wrote: > > > > Hello, > > > > I am part of the SYNTCOMP organization team this year. Ltlsynt seems > > to me the easiest tool to migrate into the, new this year, StarExec > > competition architecture. However, while trying to prepare a binary, I > > found that spot generates 1. a .libs folder with libraries 2. very > > large dependencies like libspot.so > > > > Is there a way to generate a statically-liked ltlsynt binary with no > > hidden dependencies and without all of spot in a dynamically-liked > > file? (E.g. an option like "make ltlsynt" would be ideal.) > > Hi Guillarmo, > > Like any libtool-based project, you can generate a statically-linked version > of the Spot binaries with > > ./configure --disable-shared --enable-static make -j4 > > (don't forget to run "make clean" first if you are doing this on a previous > build) > > -- > Alexandre Duret-Lutz > _______________________________________________ > Spot mailing list > Spot(a)lrde.epita.fr > https://lists.lrde.epita.fr/listinfo/spot

3 2

ltlsynt light
by Guillermo Perez 21 May '19

21 May '19

Hello, I am part of the SYNTCOMP organization team this year. Ltlsynt seems to me the easiest tool to migrate into the, new this year, StarExec competition architecture. However, while trying to prepare a binary, I found that spot generates 1. a .libs folder with libraries 2. very large dependencies like libspot.so Is there a way to generate a statically-liked ltlsynt binary with no hidden dependencies and without all of spot in a dynamically-liked file? (E.g. an option like "make ltlsynt" would be ideal.) Best, Guillermo A. Perez

2 1

Re: [Spot] syntactic stutter-invariance
by Victor Khomenko 19 May '19

19 May '19

Hi Alexandre, > Meanwhile, I have implemented SVA's first_match and ##[i:j]. > > The latter is just syntactic sugar: > a ##[i:j] b = a:([*i:j];b) > ##[i:j] b = [*i:j];b > ##i = ##[i:i] While you are at this, maybe you could also implement SVA's ##[*] and ##[+] (as sugar for ##[0:$] and ##[1:$]) for completeness? Please also note that the equality a ##[i:j] b = a:([*i:j];b) is wrong (despite being recommended in some textbooks!), e.g. {empty_word} ##[0:1] {a} =[by definition] = ({empty_word} ##0 {a}) | ({empty_word} ##1 {a}) = {} | {a} = {a} but {empty_word} : ([*0:1];{a}) = {} The reason is that ##0 always loses the empty word. Hence, it's best to split off ##0 (fusion) from ##[i>0:j] (union of concatenations) and handle them separately. Regards, Victor.

2 2

Spot bug?
by Victor Khomenko 19 May '19

19 May '19

Hi Alexandre, I've just tried to use the development version at https://spot-dev.lrde.epita.fr/app/ and fed it the following formula (which is ugly but simple, just {SERE} |-> bool), and it died of "500 Internal Server Error". {(((((((!"a")##1(!"b"))##0("c" <-> "d"))##0("e" xor "f"))##0(((((("g" & "h") xor "i") <-> "j") | "k") & "l") | "m"))##0(("n" & "o") | (!"n" & "p")))##0("q" -> ("r" <-> "s")))##[0:1]"t"} |-> "u" Regards, Victor.

2 2

Re: [Spot] syntactic stutter-invariance
by Victor Khomenko 13 May '19

13 May '19

Hi Alexandre, I've now worked out the proofs for the ## operator - there were a few (nice) surprises. To summarise, ##[i:j] is SI if both operands are SI, j is in {0,1,$}, and either: * i=0, or * i=1 and a is prefix-closed OR b is suffix-closed, or * i=2 and a is prefix-closed AND b is suffix-closed. Note that ##[0:1] does not need prefix/suffix-closedness as K:L catches some of the un-stuttered words from K;L, and similarly for ##[0:$]. These operators mix fusion with concatenation in a confusing way. Similarly, ##[2:$] was somewhat unexpected but nice :-) - I had expected only 0,1,$ to be allowed. Concerning the |=>, I hope we can lift the prefix/suffix-closedness idea to omega-languages and handle it. I also hope this will handle some cases of X, which would be really nice. E.g.: {a[+]} |=> Fx is si, and for the same reason {a[+]}|->XFx is si. Regards, Victor.

1 0

Re: [Spot] syntactic stutter-invariance
by Victor Khomenko 10 May '19

10 May '19

Hi Alexandre, I've reconsidered first_match, apparently my suggestion to eliminate the exit arcs of the accepting states in the NFA is wrong, e.g. for (a|a;a) the NFA has two accepting states with no exit arcs and the transformation does not have any effect, whereas first_match(a|a;a)=a. I guess the automaton has to be determinised before applying this transformation (unless you have a better idea). Regards, Victor. > -----Original Message----- > From: Alexandre Duret-Lutz <adl(a)lrde.epita.fr> > Sent: Tuesday, May 7, 2019 3:15 PM > To: Victor Khomenko <victor.khomenko(a)newcastle.ac.uk> > Cc: spot <spot(a)lrde.epita.fr> > Subject: Re: [Spot] syntactic stutter-invariance > > On Tue, May 7, 2019 at 10:41 AM Victor Khomenko > <victor.khomenko(a)newcastle.ac.uk> wrote: > > I have machine proofs for most of these, including the proof that K;L is si > if both K and L are si and either K is prefix-closed or L is suffix-closed. > > Interesting. > > >> a ##[i:j] b = a:([*i:j];b) > > Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof > yet. > > That would not work when B=[*0], because A:[*0] = false. However if you > assume that B has at least one letter, I believe that works. > > In the case of "a ##[i:j] b" if i>0 Spot actually rewrite this as "a;[*i-1:j-1];b" > without using ":". > > > I'd add: > > first_match(L+)= first_match(L) [* is already handled by your rules] > > So the general case is first_match(L[*i:j]) = first_match(L[*i]). > And if L is boolean, this becomes just L[*i]. > > > first_match(K;L)= first_match(K) if the empty word is in L > > first_match(K;L)= K;first_match(L) [correct?? It would then > > imply the above rule] > > That last rule doesn't look right to me. > > first_match(a[*];b[*]) = [*0] > a[*];first_match(b[*]) = a[*] > > Maybe that rule works if all words accepted by K have the same length. > (So for an easier rule, if K is Boolean). > > So to summarize, assuming b is Boolean, e accepts empty words, and f, and > g are anything else: > first_match(b[*i..j]) = b[*i] > first_match(f[*i..j]) = first_match(f[*i]) > first_match(b;f) = b;first_match(f) > first_match(f;g[*i..j]) = first_match(f;g[*i]) > first_match(f;e) = first_match(f) > It's not clear that any of those is going to improve the output > -- > Alexandre Duret-Lutz

2 1

Re: [Spot] syntactic stutter-invariance
by Victor Khomenko 07 May '19

07 May '19

Hi Alexandre, > Can we detect prefix- or suffix-closure syntactically? Not sure about omega-languages, but for the "usual" ones the prefix- and suffix-closed languages are closed wrt. | && ; + * at least (and so the derived operations). Not sure about ":", but hope so. Definitely not closed wrt. complement (prefix- and suffix-closed languages always contain the empty word, which is not in the complement). I hope these can be generalized to suffix-closed omega languages. I have machine proofs for most of these, including the proof that K;L is si if both K and L are si and either K is prefix-closed or L is suffix-closed. > Meanwhile, I have implemented SVA's first_match and ##[i:j]. Excellent news! > a ##[i:j] b = a:([*i:j];b) Do you know whether A:(B;C)=(A:B);C ? I'd guess yes, but have no proof yet. Generally, what properties does ":" have? > The former is a new operator, with three automatic simplifications: > first_match(b) = b if b is Boolean, > first_match(first_match(r)) = first_match(r), > first_match(r) = [*0] if r accepts the empty word. > (this last rule makes the translation to automata works almost > automatically) I'd add: first_match(L+)= first_match(L) [* is already handled by your rules] first_match(K;L)= first_match(K) if the empty word is in L first_match(K;L)= K;first_match(L) [correct?? It would then imply the above rule] Regards, Victor.

2 1