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
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
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.
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.
