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
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
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.
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.
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.
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
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.
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.
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.
Thanks Alexandre,
> The syntactic SI subset we catch should correspond to siPSL. (If you know a
> larger subset, that would be a welcome addition.)
What I'd like is to extend the ssi syntax to "sugar" operators too. Unfortunately, my intuition is unreliable with ssi :-(
To recap, Dax et. al. syntax for siSERE is:
r ::= [*0] | b[+] | b[*];r | r;b[*] | r:r | r|r | r&&r | r[:+]
I believe one can add the following:
- b[*], as b[*]=([*0] | b+), e.g. Spot doesn't recognise it's ssi
- (r & r), as (A & B) = (A;[*] && B)| (A && B;[*])
- any_formula[*0], as it's [*0]
- if the overall formula is {b}, it's ssi.
Another problem is that, say, (a[*];b[*]);(c[*];d[*]) is not ssi, but can be transformed to ssi form using associativity of ";".
Now, for special cases of i and j, the r[*i:j], b[*i:j], r[=i:j], r[->i:j] may be ssi (I tried to work these out, but was confused by the {a[=2:3]}|->b result).
PSL closures:
cl(r) is part of ssi syntax so ok
not sure about {r} - it might be obvious, but I don't understand closures well, especially if negations are involved...
{r}! is equivalent to {r}|->1, so I think it's ssi
Bindings: |-> is ssi, but I'm not sure about when |=> might be ssi?
If you ever going to support SVA-like "throughout" and "within", they are ssi:
A throughout B = (A* && B), A is Boolean
A within B = (([*];A;[*]) && B)
Also, SVA's first_match operator is interesting - do you know of a general way of translating it to other operators, or, alternatively, do you plan to ever add it? (BTW, it would also be nice to have C-like ternary operator ?: to avoid the exponential blow-up in its translation.)
> > {a[->2:3]}|->b
> I can't reproduce this one. It is shown as stutter-sensitive for me.
Sorry, my bad, it's indeed ss.
Thanks,
Victor.
