- Spot - LRE

Issues running examples
by Jiraphapa Jiravaraphan 03 Jun '19

03 Jun '19

Dear Spot team, I am trying to get Spot 2.7.4 running on macOS (tarball installation), the command-line tools works properly on terminal, however, trying to run Python and C++ examples does not work. *For C++:* output from on-the-fly Kripke structure example (from https://spot.lrde.epita.fr/tut51.html) $ g++ -std=c++14 kripkeTest.cc -lspot -o kripkeTest Undefined symbols for architecture x86_64: "_bdd_addref_nc", referenced from: bdd::operator=(bdd const&) in kripkeTest-6ae779.o bdd::bdd(bdd const&) in kripkeTest-6ae779.o bdd::bdd(int) in kripkeTest-6ae779.o "_bdd_apply", referenced from: bdd_apply(bdd const&, bdd const&, int) in kripkeTest-6ae779.o "_bdd_delref_nc", referenced from: bdd::operator=(bdd const&) in kripkeTest-6ae779.o bdd::~bdd() in kripkeTest-6ae779.o "_bdd_not", referenced from: bdd_not(bdd const&) in kripkeTest-6ae779.o "_main", referenced from: implicit entry/start for main executable ld: symbol(s) not found for architecture x86_64 clang: *error: *linker command failed with exit code 1 (use -v to see invocation) (I could only run helloword.cc example) *For Python:* trying to run example on Kripke structure using source code from https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html $ python3 Python 3.7.3 (v3.7.3:ef4ec6ed12, Mar 25 2019, 16:39:00) [GCC 4.2.1 (Apple Inc. build 5666) (dot 3)] on darwin Type "help", "copyright", "credits" or "license" for more information. >>> import spot >>> import spot.ltsmin >>> spot.ltsmin.require('divine') divine not available (I think there has something to do with the path because I have to manually add spot directory into pythonpath in order to be able to import spot even if I use ./configure, make, make install) Any insights 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

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

07 May '19

Hi Alexandre, > However now that you have written this down, I think your interpretation r > SSI => r[+] SSI and r[*] SSI is also sound, but I have no proof for this. I tried to prove this, but failed, and then found a counterexample: e.g. if L = a[+];(!a)[+];a[+], then L is si but both L[+] and L[*] are not si. I believe if one in addition requires that L is prefix-closed or suffix-closed, then the result would hold (I have an idea how to prove this). > > > I would suggest that at the SERE level the rule for the n-ary > concatenation > > > r1;r2;r3;...;rn > > > could be extended so that the entire concatenation is SSI iff each > > > ri is SSI and at most one of them rejects the empty word. Again, this seems wrong, with the following counterexample: If K=[*0] | ((!a)[+] ; a[+]) and L=a[+] then K contains the empty word, K and L are si, but K;L is not si: it accepts !a;a;a but rejects !a;a. I think the result would hold if one replaces the assumption that K or L contains the empty word by K being prefix-closed or L being suffix-closed. > > > Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff > > > - s and t are both SSI, and > > > - s recognizes the empty word Again, I think we could require either s being prefix-closed or t being suffix-closed. Note the symmetry with s;t :-) Regards, Victor.

2 1

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

29 Apr '19

Hi Alexandre, > Currently r[*i:j] is SSI iff j=inf and i<=1 (used to be i==1 before your mail). I'm not sure if this is correct, as it implies that r* is ssi if r is ssi, even if r is not a Boolean, but Dax at al. mentioned that the use of * has to be restricted (but without giving an example of ssi violation). So it's your word against theirs :-) Do you have a proof? (I played with Spot a couple of minutes and could not quickly find a violation, so you may well be right.) > [=i:j] and [->i:j] are sugar on top of ; and [*i:j], so it follows from those > definitions. > (Spot's AST has no representation of those operators, they only exist in the > parser and printer.) The situation with [=i:j] and [->i:j] is less boring than that! E.g. b[->1:$] would be translated to something like (!b[*];b)[+], which is si but not ssi. I've worked out the cases for these operators as follows (the proofs rely on the magic regex equivalence (a[*];b)[+];a[*] = (a|b)[*];b[+] which can be checked e.g. here: https://regex-equality.herokuapp.com/) Lemma: b[->i:j] is si iff j=0 or (j=$ and i<=1) j=0: then i=0 and so b[->i..j] = (!b[*];b)[*0] = [*0], so si j!=0 and j!=$: then b[->i..j] accepts b[*j] but not b[*j+1], so not si j=$ and i>1: then b[->i..j] accepts b[*i] but not b[*i-1], so not si j=$ and i=1: then b[->i..j]=(!b[*];b)[+]=[by regex magic]=(!b|b)[*];b[+]=[*];b[+], so si j=$ and i=0: then b[->i..j]=(!b[*];b)[*]=[*0]|above line, so si Lemma: b[=i:j] is si iff j=0 or (j=$ and i<=1) j=0: then i=0 and so b[=i..j] = (!b[*];b)[*0];!b[*] = !b[*], so si j!=0 and j!=$: then b[=i..j] accepts b[*j] but not b[*j+1], so not si j=$ and i>1: then b[=i..j] accepts b[*i] but not b[*i-1], so not si j=$ and i=1: then b[=i..j] = (!b[*];b)[+];!b[*] = [by regex magic] = (!b|b)[*];b[+];!b[*] = [*];b[+];!b[*], so si j=$ and i=0: then b[=i..j] = (!b[*];b)[*]];!b[*] = (e|(!b[*];b)[+]);!b[*] = !b[*] | (!b[*];b)[+];!b[*] = [due to previous case] = !b[*] | [*];b[+];!b[*] = [*] so si > cl(r) in Dax et al. is the same as {r} in Spot. > > But you are not the only one having trouble with closure :-) See > https://gitlab.lrde.epita.fr/spot/spot/issues/242 So, just to confirm, Dax et al.'s cl(), PSL's {}, and Spot's {} are all the same, aren't they? > I would suggest that at the SERE level the rule for the n-ary concatenation > r1;r2;r3;...;rn > could be extended so that the entire concatenation is SSI iff each ri is SSI and > at most one of them rejects the empty word. Wow, that is a nice generalisation! Do you have a proof? I think it will be nicer and easier to state for the binary ";", and then the n-ary case immediately follows. > Transposed to {s}|=>t, that rule would state that {s}|=>t is SSI iff > - s and t are both SSI, and > - s recognizes the empty word I did some experiments with the online tool, and what you say seems correct, but I don't understand why there is asymmetry w.r.t. s (but not t) recognising the empty word - the intuition of s;t seems symmetric? > If we had complementation of SERE, would first_match(r) be implementable > as r && ((!r);1[+]) ? I think you meant r && !(r;[+]), which is a nice idea, but Spot won't accept it (I guess), and generally it seems computationally expensive. I think at the level of automata one can simply get an NFA for r, and then delete all arcs from accepting states? The other things you mentioned, like $rose etc. seem to need past modalities? Or you can mix state-based and action-based logics? Generally, "throughout" and "within" are just syntactic sugar, so should be easy to add. The ?: can be added as syntax sugar, but hopefully one can do better than that and avoid the exponential blow-up due to repeating A in A&B|!A&C - this is in fact just a theoretical blow-up, unlikely to happen in practice. The first_match requires some work with automata, but seems possible. I'd say Spot is just a few steps away from full alignment with SVA and PSL. Regards, Victor.

2 1