- Spot - LRE

Bug in ltlsynt - lar algorithm
by Guillermo Alberto Perez 18 Jun '19

18 Jun '19

Hello, While running tests for SYNTCOMP 2019 we found that ltlsynt outputs an incorrect controller on one of our benchmarks: simple_arbiter_enc_2.tlsf (available from https://bitbucket.org/swenjacobs/syntcomp/src/master/SelectedBenchmarks2018…) I am calling the tool with --aiger --algo=lar and using iimc as our model checker. Best, Guillermo

2 3

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

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