- Spot - LRE

ltl2tgba: diagnostics for stutter-sensitive properties
by Victor Khomenko 21 Nov '19

21 Nov '19

Hi Alexandre, Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be possible to print a warning with diagnostics, like the online tool does? Something like: Warning: The property is stutter-sensitive - the following words are a proof, as they differ only by some stuttering: Accepted word: a & b; a & b; cycle{!a & !b} Rejected word: a & b; cycle{!a & !b} Motivation: * by passing the option --check=stutter-invariant the user tells the tool that stutter-invariance is important for them, hence a warning/diagnostics is desirable if the check fails (this warning does not have to be printed if this option is not passed) * it's not easy to get these traces from the final automaton - my understanding is that some potentially costly operations are required, which are performed during the check anyway * the current way of getting this diagnostics (python + libraries; maybe there is a better way I don't know about?) creates many dependencies, thus making it difficult to integrate this functionality into toolchains - ideally one would want just a single executable ltl2tgba * my (perhaps naive) understanding is that this is not difficult to implement and does not incur much extra run-time as the check has to be performed anyway Best regards, Victor.

2 1

Re: [Spot] command-line option to negate input formula
by Victor Khomenko 24 Sep '19

24 Sep '19

> > Could you add a command-line option for ltl2tgba to invert the input > formula before computing the automaton? > > Done. > https://gitlab.lrde.epita.fr/spot/spot/commit/7f21d3ff29ad3a513f261025c5 > 75e4676a14cc50 Great - many thanks! > Any opinion on what passing --negate twice should do? A really good and nerdy one - twice the smiley face! :-) :-) Cheers, Victor.

1 0

command-line option to negate input formula
by Victor Khomenko 24 Sep '19

24 Sep '19

Hi, Could you add a command-line option for ltl2tgba to invert the input formula before computing the automaton? Yes, it's trivial to do externally, but there are good reasons to have this option: * this would remove an extra step from model checking toolchains (where the automaton is built for the negation of a formula) * if the formula goes through a toolchain, it's better to keep equivalence all the way through to the automata, so that the user can easily see that the property has not been broken by transformations, and also comprehend any formula-related diagnostics logged by the tools. Thanks, Victor.

2 1

LTLf formulas
by Yong Li (李勇) 10 Sep '19

10 Sep '19

Dear Spot developers, I am Yong Li from Chinese Academy of Sciences and I am writing to you to ask a question about parsing LTLf (LTL over finite traces) formulas. Spot supports LTL with finite semantics (LTLf) but I found out that Spot eagerly simplifies the input formulas with LTL semantics. For instance, if I use command line ltlfilt --from-ltlf -f "a U !(X True)", Spot immediately gives me 0. This is not correct since the input formula should be satisfiable in LTLf semantics. I wonder whether there is a way to get around it? Is there a an option I can use to make Spot parse the formula without simplying it? Regards, Yong

2 1

Issue with SPOT and LTLf
by Andrew Wells 28 Aug '19

28 Aug '19

I'm trying to use SPOT to build an automaton for an LTLf formula, but I think there is a bug. I'm using this code (based on https://spot.lrde.epita.fr/tut12.html) #include <iostream> #include <spot/tl/ltlf.hh> #include <spot/tl/parse.hh> #include <spot/twaalgos/hoa.hh> #include <spot/twaalgos/remprop.hh> #include <spot/twaalgos/translate.hh> int main() { spot::parsed_formula pf = spot::parse_infix_psl("((a && b) U (! (X 1)))"); if (pf.format_errors(std::cerr)) return 1; spot::translator trans; trans.set_type(spot::postprocessor::BA); trans.set_pref(spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf.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 aut = post.run(aut); print_hoa(std::cout, aut) << '\n'; return 0; } In LTL, this would be a contradiction, but in LTLf it is not as the next operator cannot be true at the last timestep. There seems to be an issue with SPOT where it simplifies the automaton as though the formula is in LTL, yielding an incorrect automaton. Am I using this correctly? I'd be willing to write a patch if this is indeed a bug. Thanks, Andrew Wells

2 1

Change log from version 2.0 to 2.8
by M. H. Zibaeenejad 24 Aug '19

24 Aug '19

Hi, I have used the version 2.0 of your online tool for LTL to Buchi automata translation. At the time the tool did not return a deterministic Buchi automaton, but the new version does the transformation with ease. I was wondering if something fundamental has changed in your code that made this possible. Do you have the Changelog from 2.0 to 2.8? Here is the formula i used : G(!e) & G((c&!d&Fd)->(p Ud)) & G(a&!c->(!c W(b&!c))) & GF(a)&GF(b)&GF(c)&GF(d) RegardsHadi Zibaeenejad,PhDUniversity of Waterloo

2 1

Compiling Spot on windows
by Maxime Bouton 04 Jul '19

04 Jul '19

Dear Spot maintainers, I was wondering if there had been some work on compiling Spot with the python bindings on windows? I have been able to create windows binaries for libspot.so using a cross-compilation environment and mingw with the option `--disable-python`, and I saw that there was a similar example in the continuous integration configuration on gitlab. However I would be interested in having the python bindings as well. * Do you think it is possible for one to get the python bindings for windows? * Do you have any hints on how one could proceed? In the cross-compilation environment I had an error in the `./configure` step, related to not being able to find `python.h` on the target (windows 64bits) and was not able to make much progress in that direction. Thanks for your help, Maxime

2 2

Theorem question
by Scott M. Staley 30 Jun '19

30 Jun '19

Hi all, A quick (?) question. When I put the following LTL formula into SPOT online: G (G (p => Gp ) => Gp) => (FG p => Gp) SPOT says it is equivalent to 1. Therefore I assume it’s a theorem of LTL. My question: Is there anyway to see the series of rewrites of the formula to show how it gets form the original formula to “true”? Thanks, Scott

2 1

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

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

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

27 Apr '19

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.

2 1

syntactic stutter-invariance
by Victor Khomenko 26 Apr '19

26 Apr '19

Dear Spotters, Could anyone explain Spot's algorithm for checking whether a PSL formula is syntactically stutter-invariant (ssi), including all supported PSL operators? I'm aware of Dax et al. ATVA'09 paper, but the syntax there is rather rudimentary, and there seems to be more to this. E.g. {a[=2:3]}|->b is rewritten (using the online spot's toolkit) into a R (!a | X({a[->1..2]}[]-> (b & X(b W a)))) and yet it is classified as ssi in spite of all the Xs. On the other hand, a seemingly similar {a[->2:3]}|->b is classified as si but not ssi for some reason... Many thanks, Victor.

2 1

Bug if generating deterministic Emerson-Lei
by David Müller 26 Apr '19

26 Apr '19

Hi Alexandre, I run the experiments and found two formulas where ltl2tgba did not finish correctly. The formulas were & | G F p0 F G p1 | G F ! p1 F G p2 & & | G F p0 F G p1 | G F ! p1 F G p2 | G F ! p2 F G ! p0 The according command-line was: ltl2tgba -D --generic -C -S --lbt-input -f ${FORMULA} Output was: ltl2tgba: direct_simulation() requires separate Inf and Fin sets Best, David

2 1

check equivalence from files?
by Stephen Siegel 05 Apr '19

05 Apr '19

Question about the command line interface. I know something like ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a’ can be used to determine if two LTL formulas are equivalent. Is there a way to do that if both formulas are in files? From the man page I could only see how to make the first formula come from a file (-F).

2 1

Spot documentation
by Yannick Molinghen 03 Apr '19

03 Apr '19

Dear Madam, dear Sir, I am just starting using spot (with python) for a university project (ULB, Brussels) and my team mates and I have spent quite some time just figuring out how to use accepting states in a Buchi automaton. We found it inconvenient and more importantly very difficult to find in the documentation (it was located in the far end of the doc...) to use `automaton.prop_state_acc(True)` in order to set states accepting instead of edges. It could be interesting to specify how to do this in a clear way, why not in the code examples? A good place for this would be this page <https://spot.lrde.epita.fr/tut22.html> for instance. Yours sincerely, Yannick Molinghen

2 1

Exclusive-AP and Merge Transitions
by hashim ali 01 Apr '19

01 Apr '19

Hi, How can I use Exclusive-AP and merge transitions in python to reduce my automaton and the number of transitions? An example would suffice. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 1

Highlight Words on the Automaton
by hashim ali 01 Apr '19

01 Apr '19

Hi, Similar to highlighting runs on the automaton, is it possible that I can convert a word to a corresponding run and then I can highlight it on the automaton? Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 1

Generate Words for verification
by hashim ali 27 Mar '19

27 Mar '19

Hi, I am using spot.from_ltlf().translate() to translate LTL rules into a finite automata (with alive property). Now I want to verify certain words that whether they are accepted by the automata or not. These words will be generated from a powerset of the set of atomic propositions. Lets suppose I have AP = {a,b,c,d}. How do I generate words from the powerset of AP and verify it on the automata. Should the word always contain a cycle and a prefix part. If yes, what should be the cycle part and what should be the prefix part. I will be waiting for your response. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 4

Weighted Automata
by hashim ali 25 Mar '19

25 Mar '19

Hi, Is there any support for weighted Automata in spot. Here is a thing I want to implement. I want to test certain words on a certain automata, if a word is rejected by the automata I want to add a new transition (weighted transition) to this automata and later on if that same word comes for verification, I want this automata to return this weight corresponding to this transition. Thanks and Regards, Hashim Ali Research Assistant Laboratory for Cyber-Physical Networks and Systems (Cyphynets) Lahore University of Management Sciences (LUMS)

2 1

C interface for Spot?
by Stephen Siegel 25 Mar '19

25 Mar '19

Is there a C (not C++) interface for Spot? I want to call Spot from my C program. Thanks.

2 1

Re: [Spot] Questions regarding handling of Kripke structures in Spot
by Alexandre Duret-Lutz 05 Mar '19

05 Mar '19

Dear Patrick, (Please keep the mailing list in copy so that these explanations get archived and then indexed by search engines.) On Tue, Mar 5, 2019 at 8:58 AM Halder, Patrick <patrick.halder(a)tum.de> wrote: > When I have the twa_product automaton with its respective acceptance states, > how can I find out, to which states of my original Kripke structure they correspond to. > I read somewhere in the spot examples that the labeling of the twa_product states > (of the form <*,*>) has just cosmetic reasons and does therefor not give any help. Let's say you have built the product between two automata autx and auty: prod = spot.product(autx, auty) then pairs = prod.get_product_states() will return an array of pairs of the form [(x0,y0),(x1,y1),....]. State i in the product corresponds to states pairs[i][0] in autx, and pairs[i][1] in auty. See https://spot.lrde.epita.fr/ipynb/product.html around cell 10 for a concrete example, and a tip about using show("1") in this context. > Is it even possible to do this, meaning getting directly from the acc states of the product automaton to the acc states/runs of the Kripke structure? You should probably look for the accepting SCCs of the product, not only its accepting states. You could list all states that belong to acceptings SCCs of the product with something like si = spot.scc_info(prod) n = si.scc_count() for i in range(n): if si.is_accepting_scc(i): for s in si.states_of(i): print(s) Unfortunately, we do not yet have any online example of use of scc_info in Python. You can find some in the test suite, or simply look at the C++ documentation for this class https://spot.lrde.epita.fr/doxygen/classspot_1_1scc__info.html > Or do I have to get the accepting runs of the product automaton, e.g., with the x.intersecting_run(y) method and reason with it about the accepting runs in the Kripke structure? This will only return one accepting run. -- Alexandre Duret-Lutz

1 0

SPOT
by Alina Florina Popa /Student 01 Mar '19

01 Mar '19

Hello, I am trying to convert a LTL formula to Buchi automata in MATLAB. I want to know if you have any script or library that can help me do this? Thank you and best regards, Alina Popa -- Fourth-year Student | Automatic Control and Applied Informatics | Systems Engineering Faculty of Automatic Control and Computer Engineering “Gheorghe Asachi” Technical University of Iasi, Romania www.ac.tuiasi.ro <http://www.ac.tuiasi.ro/> | www.tuiasi.ro <http://www.tuiasi.ro/>

2 1

Questions regarding handling of Kripke structures in Spot
by Halder, Patrick 21 Feb '19

21 Feb '19

Dear Spot Team, I'm a master's student at Technical University of Munich and I'm currently writing my Master's Thesis in the research field of path planning for autonomous cars. I came across Spot on the internet and I think it's a very nice tool that fits exactly my needs: I've got a discrete finite automaton (with certain attributes/APs per node) and I want to check, if this automaton satisfies a certain LTL specification. Especially, my intention is to find all path in my automaton, that satisfy a LTL specification. I've already installed Spot on my computer and tried to implement this with Python. Now I've got the following two questions: 1. What is the most simple and fastest way of defining a spot kripke graph, based on my own automaton (which is basically just a dictionary with nodes, that hold certain attributes and parent/child relations) ? Is there a possibility of including my nodes and transitions step by step into a spot kripke graph or do I have to convert my automaton at first into e.g. the HOA format and afterwards import this HOA-string as a kripke graph? 2. Building the product of a LTL formula (resp. the Büchi automaton) with the kripke graph leads to a object of the class twa_product. Is there a possibility of transforming this product back into a kripke structure or exporting it as a simple dictionary, so that I can make further computations on this "reduced" graph? I hope you can help me with my questions and maybe provide some simple code examples. Thank you very much in advance! Yours sincerely, Patrick Halder

2 1

UBA-generation of ltl2tgba
by Simon Jantsch 12 Feb '19

12 Feb '19

Hello, I have noticed two types of errors that seem to occur when telling ltl2tgba to output unambiguous Büchi automata (UBA). One seems to be some kind of assertion triggering and happens only in combination with the flag „—low“. That is, on running: ltl2tgba —low -U -B -f $FRML the tool occasionally exits with exit code 2 and: „ltl2tgba: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true“ This happens for example for the formula: (G(!(G("2")))) & (("1") | (F("2"))) In some cases the UBA generated by ltl2tgba seem to be incorrect as well, and I don’t think this has to do with the „—low“ flag. An example formula is (("2") W (G("1"))) -> (G("1")) To reproduce these behaviors you can run ltlcross on the attached file „error“, as follows: cat error | ltlcross —-lbt-input ‚ltl2tgba -U -B —-low -f %f >%O' 'ltl2tgba -f %f >%O' Best regards, Simon

2 1

_impl issue with install
by Lonnie Parker 06 Jan '19

06 Jan '19

Hello, I'm new to spot and a bit of a novice with coding in general but I've been running into an issue related to one of the modules that comes with spot when attempting to run python code using the spot python bindings: File "/usr/lib/python3.6/importlib/__init__.py", line 126, in import_module return _bootstrap._gcd_import(name[level:], package, level) ModuleNotFoundError: No module named '_impl' I understand if it is too difficult to diagnose with the limited output, but I didn't want to bombard anyone with lengthy output. I am running Ubuntu 18.04 (Bionic Beaver) and have successfully installed spot using ./configure, make, make install. Prior to installing spot, I also installed the latest version of swig. I've also verified that the relevant .so files are located within my .local/lib/python3.6/site-packages/spot directory. If this issue with using import_module to locate the _impl package looks familiar, any information would be much appreciated. Thank you! Best, Lonnie -- "But as for you, promote the kind of living that promotes right teaching." --Titus 2:1

2 1

partial order reduction and stuttering
by Stephen Siegel 11 Dec '18

11 Dec '18

The web page https://spot.lrde.epita.fr/ipynb/stutter-inv.html shows how to use Spot to highlight the states in a Büchi automaton which have a stutter invariant language. It says "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton.” Does anyone know a reference for this technique? I mean specifically the idea that POR is something that can be turned on or off depending on the current state of the property automaton. I feel I’ve seen that somewhere, but don’t remember where. Thanks! -Steve

2 1

spot's website is down
by 刘天池 07 Dec '18

07 Dec '18

Hello: I want know why all website about spot is down. website list: https://spot.lrde.epita.fr/ https://www.lrde.epita.fr/mailman/listinfo/spot-announce best regards! Tianchi Liu from ECNU

2 1

Spot build fails
by Maxime Bouton 11 Nov '18

11 Nov '18

Hello, I am trying to set up a automated build for Spot in a docker like environment. The build errored during the `make` step. I have been able to run it fine on my machine, so I hope it is just a dependency/version issue. Do you have any idea what dependency I could be missing? I did not installed anything besides python3-dev and got provided with an alpine linux distribution with gcc 7 already installed, this is the configuration I have: Configuration: OS: Alpine Linux Gcc --version: gcc (GCC) 7.1.0 G++ --version : g++ (GCC) 7.1.0 Clang --version: clang version 6.0.1 Spot source: https://gitlab.lrde.epita.fr/spot/spot/-/jobs/21303/artifacts/download (spot 2.6.3 dev) The build script : apk add python3-dev cd $WORKSPACE/srcdir unzip download tar -xzf spot-2.6.3.dev.tar.gz cd spot-2.6.3.dev ./configure --prefix=$prefix --host=${target} make -j${nproc} make install Extract of the log : make[3]: Entering directory '/workspace/srcdir/spot-2.6.3.dev/spot/misc' /bin/bash ../../libtool --tag=CXX --mode=compile /opt/x86_64-linux-gnu/bin/x86_64-linux-gnu-g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -W -Wall -Werror -Wzero-as-null-pointer-constant -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Wmissing-declarations -Wnoexcept -Woverloaded-virtual -Wmisleading-indentation -Wimplicit-fallthrough -Wlogical-op -Wduplicated-cond -Wnull-dereference -Wsuggest-override -Wpedantic -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c -o tmpfile.lo tmpfile.cc libtool: compile: /opt/x86_64-linux-gnu/bin/x86_64-linux-gnu-g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -W -Wall -Werror -Wzero-as-null-pointer-constant -Wcast-align -Wpointer-arith -Wwrite-strings -Wcast-qual -DXTSTRINGDEFINES -Wmissing-declarations -Wnoexcept -Woverloaded-virtual -Wmisleading-indentation -Wimplicit-fallthrough -Wlogical-op -Wduplicated-cond -Wnull-dereference -Wsuggest-override -Wpedantic -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c tmpfile.cc -fPIC -DPIC -o .libs/tmpfile.o tmpfile.cc: In function 'const char* spot::{anonymous}::get_tmpdir()': tmpfile.cc:38:25: error: 'secure_getenv' was not declared in this scope const char* res = secure_getenv("SPOT_TMPDIR"); ^~~~~~~~~~~~~ tmpfile.cc:38:25: note: suggested alternative: '__secure_getenv' const char* res = secure_getenv("SPOT_TMPDIR"); ^~~~~~~~~~~~~ __secure_getenv tmpfile.cc: In destructor 'virtual spot::temporary_file::~temporary_file()': tmpfile.cc:91:32: error: 'secure_getenv' was not declared in this scope static bool must_unlink = !secure_getenv("SPOT_TMPKEEP"); ^~~~~~~~~~~~~ tmpfile.cc:91:32: note: suggested alternative: '__secure_getenv' static bool must_unlink = !secure_getenv("SPOT_TMPKEEP"); ^~~~~~~~~~~~~ __secure_getenv make[3]: *** [Makefile:1284: tmpfile.lo] Error 1 make[3]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev/spot/misc' make[2]: *** [Makefile:1357: all-recursive] Error 1 make[2]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev/spot' make[1]: *** [Makefile:1274: all-recursive] Error 1 make[1]: Leaving directory '/workspace/srcdir/spot-2.6.3.dev' make: *** [Makefile:1194: all] Error 2

2 3

Compilation under Cygwin
by Jerry Swan 29 Oct '18

29 Oct '18

Hi, I'm attempting to compile under cygwin. Calling configure (with --disable-python) succeeds, but make fails (with error message as below). The problem would appear to be the absence of 'secure_getenv', though FWIW the generated makefile contains 'HAVE_SECURE_GETENV = 0'. Any pointers on how I might get this to compile (preferably with minimum disruption to the source or build process)? Thanks and best wishes, Jerry. =============================== Error message: /bin/sh ../../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c -o tmpfile.lo tmpfile.cc libtool: compile: g++ -DHAVE_CONFIG_H -I. -I../.. -I../.. -I../.. -I../../buddy/src -I../../lib -I../../lib -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++14 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT tmpfile.lo -MD -MP -MF .deps/tmpfile.Tpo -c tmpfile.cc -DDLL_EXPORT -DPIC -o .libs/tmpfile.o tmpfile.cc: In function ‘const char* spot::{anonymous}::get_tmpdir()’: tmpfile.cc:36:25: error: ‘secure_getenv’ was not declared in this scope const char* res = secure_getenv("SPOT_TMPDIR"); ^~~~~~~~~~~~~ tmpfile.cc: In destructor ‘virtual spot::temporary_file::~temporary_file()’: tmpfile.cc:89:32: error: ‘secure_getenv’ was not declared in this scope static bool must_unlink = !secure_getenv("SPOT_TMPKEEP"); [...] make: *** [Makefile:1194: all] Error 2 ===============================

2 2

Julia bindings for Spot
by Maxime Bouton 05 Oct '18

05 Oct '18

Dear Spot maintainers, I am a PhD student at the Stanford Intelligent Systems Lab (SISL), we are interested in implementing a Julia wrapper for Spot. So far I have prototyped a very simple version that calls the binary to write to a .hoa file, then parse the .hoa file and build an automata structure, I tried it on very simple formulas. In the coming day I am going to call the c++ api of spot from Julia and extract the datastructure from it instead of writing my own parser. The idea would be that I can then manipulate the automata using native Julia objects. I am looking at this example from the documentation: https://spot.lrde.epita.fr/tut50.html The explicit interface seems like what I am looking for, please let me know if I am missing other relevant examples. If you are aware of some people working on this please let us know, we would be happy to contribute and join forces. Would you agree if we name the Julia package Spot.jl ? Best, Maxime

2 1

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 05 Oct '18

05 Oct '18

Dear SPoT developers, I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem. I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for. However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem. My questions are the followings: 1) Do they allow to express the same properties ? and 2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ? Kind regards, Martin.

2 1

SPoT + PSL + Dynamic Logic.
by Martin Dieguez 03 Oct '18

03 Oct '18

Dear SPoT developers, I am writing to you to ask you a question about the semantics of PSL and SPoT. I will start by explaining my problem. I am interested in computing the automata associated to a Linear Dynamic Theory under Linear Dynamic Logic semantics. The semantics can be found in the following paper: https://www.cs.rice.edu/~vardi/papers/ijcai13.pdf Although the semantics are interpreted on finite traces I would be interested in using infinite traces. I found out that SPoT allows expressing PDL regular expressions on linear (infinite) traces, which is what I was looking for. However, after checking the specification language, I found that the dynamic operators are not "exactly" the same as those of Linear Dynamic Logic. I mean, I was expecting to write [(true;true)*] p instead of {(1;1)[*]}[]->p to represent the even-state problem. My questions are the followings: 1) Do they allow to express the same properties ? and 2) How faisable is to accomodate the parser to accept the PDL syntax ? Could you give me some hints on this case ? Kind regards, Martin.

1 0

Potential Bug in Spot?
by Andreas Tollkötter 25 Sep '18

25 Sep '18

Hello, with the currently newest version of Spot 2.6.1, the following behavior occurred for me, which I would call a bug. I attached a DOT file of a deterministic parity automaton which was written by "autfilt --dot --highlight-languages". What is notable that (among other pairs), states 10 and 66 are marked as language-equivalent states. Their "a1"-successors, 30 and 62 are not equivalent however, so something must be wrong here. I assume a potential cause is that there are a total of 18 non-trivial equivalence classes but only 16 different colors defined to be used by Spot, so some are used for multiple classes? If that is the case, I feel like there should be at least a warning output by "autfilt" when this happens. Best regards, Andreas Tollkötter

2 1

ltlfilt does not exhaustively simplify when --remove-wm is enabled
by Simon Jantsch 23 Sep '18

23 Sep '18

Hello, I am confused by the fact that the following two commands do not produce the same result: ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ ltlfilt --simplify=3 --remove-wm --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --simplify=3 The first command gives the same formula as: ltlfilt --simplify=3 --lbt-input --lbt -f "W ! p0 W p0 W ! p0 W p0 G ! p0“ | ltlfilt --lbt --lbt-input --remove-wm which makes me believe that simplification is done before removing the operators M and W. I would expect ltlfilt to first remove the operators and then simplify exhaustively. Is this behavior intended and if it is, what is the best way to get an exhaustively simplified formula without certain operators? Best regards, Simon

2 1

spot-2.6.1 conflicts with libiconv-1.14: it installs the file lib/charset.alias
by Yuri 10 Aug '18

10 Aug '18

Installing spot-2.6.1... pkg-static: spot-2.6.1 conflicts with libiconv-1.14_11 (installs files into the same place). Problematic file: /usr/local/lib/charset.alias *** Error code 70 Please remove this file. Thanks! Yuri

3 4

--disable-doxygen doesn't disable doxygen
by Yuri 10 Aug '18

10 Aug '18

gmake[5]: Leaving directory '/wrkdirs/usr/ports/math/spot/work/spot-2.6.1/doc' rm -rf spot.html spot.latex doxygen gmake[4]: doxygen: Command not found Version 2.6.1 on FreeBSD. Thanks, Yuri

2 2

Multiple accepting runs for Buchi Automaton
by Thakur Neupane 10 Aug '18

10 Aug '18

Hello, I am using SPOT to work with Buchi Automaton. Does SPOT supports finding all the accepting runs instead of only one? Sincerely, Thakur Neupane

2 1

Return all accepting runs for emptiness checking
by Zhen Zhang 02 Aug '18

02 Aug '18

Hello, We would like to know if the emptiness checking algorithms for Buchi automata can return all accepting runs, instead of a single one as the tool has implemented. Thanks, Zhen Zhang

1 0

Cloning an automaton
by Ayrat Khalimov 17 Jun '18

17 Jun '18

Hello! Given a co-Buchi automaton and some number K, my function [1] creates another automaton ("co-Reachability") that bounds by K the maximal number of visits to co-Buchi accepting states. I currently create the new automaton like this: auto new_aut = make_twa_graph(aut->get_dict()) but this BDD-dictionary sharing between the new and the original automaton looks suspicious: once the original automaton dies and kills its dictionary (?), the new automaton will no longer be able to use it. Right? I guess the correct way is to create a new dictionary for the new automaton: auto new_d = spot::make_bdd_dict(); But then: what will be the natural way to copy edges of the original automaton into the new automaton? I currently simply iterate over edges of `aut` and do smth like: for (auto &t: aut->out(state)) k_aut->new_edge(src_state, dst_state, t.cond); where `t.cond` refers to a BDD of `aut`. So, I will need to create `cond` that uses new BDD dict, right? Which functions will be useful for doing that? Thanks! A minor point: If you use CUDD library and SPOT in the same project, then you will get compilation errors, because: CUDD does not use namespaces and has type `BDD`, and and Buddy in SPOT does not use namespaces and has `BDD`. To overcome the clash, the simple trick below works, but... maybe put Buddy into separate namespace? (minor feature request:) (I apologize for not providing the patch!) My current workaround is: whenever including SPOT headers, include them like this: #define BDD spotBDD #include <spot/twa/twagraph.hh> #include <spot/twaalgos/sccinfo.hh> #undef BDD best wishes, Ayrat Khalimov [1] https://github.com/5nizza/sdf-hoa/blob/master/src/k_reduce.cpp#L69

2 3

bug spot online
by MATTEO LUCCHI 22 Mar '18

22 Mar '18

Good afternoon, You are probably already aware of that, but the spot online translator is not working anymore. I am trying to translate a LTL formula into a Buchi Automaton. It was working until 2 days ago, but now i get this: Traceback (most recent call last): File "/var/www/html/cgi-bin/spotcgi.py", line 732, in <module> render_automaton(degen, dont_run_dot) File "/var/www/html/cgi-bin/spotcgi.py", line 318, in render_automaton render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 305, in render_dot_maybe render_dot(autprefix, hoaname) File "/var/www/html/cgi-bin/spotcgi.py", line 237, in render_dot run_dot(basename, 'svg') File "/var/www/html/cgi-bin/spotcgi.py", line 230, in run_dot os.link(outname, tmpdir + "/" + ext) FileNotFoundError: [Errno 2] No such file or directory: '../spotimg/960f234ef7d2cd7d8fbab23c49603c6a66fc284d.svg' -> '../spotimg/0f33f8af71a0356e3d63971bc8a4a7e39e64b7d9-154/svg' Any fix to the problem? Thank you! Kind Regards, Matteo Lucchi

2 1

A bug in determinization procedure of Spot?
by Anton Pirogov 22 Mar '18

22 Mar '18

Hello, first I just want to say, thanks for creating Spot, it is immensely useful! And I think that I might have found a bug (or two). My inputs are classic state-based NBAs. I rely on Spot to compare and verify my determinized automata, i.e. I compare the automaton that my tool produces with the one I get from Spot using autfilt -D -S -p (to get a deterministic parity automaton). I use autfilt --equivalent-to=... for the equivalence test. Yesterday I noticed something strange. When I compare the original NBA and my DPA, it reports that they are equivalent. Same for the original NBA and the DPA I get from Spot. But when I compare my automaton with the one from Spot, it says that the languages are different! So the first thought was - something must be broken in the equivalence test. Apparently, at least one of the three answers I got is wrong. So I used a little Python script using the Spot API to get a word where two of the automata do not agree on. Let's call the original NBA A, my DPA B and the one from Spot C. There were no words found in A×¬B, ¬A×B, A×¬C, ¬A×C and also B×¬C. But there IS a word in ¬B×C. I used this word with autfilt --accept-word=... to check A, B and C. And it turned out that in fact A and B do not accept the word, but C does, i.e. C is incorrect. So, to conclude, there seems to be a bug in the determinization and the problem is not detected by the equivalence test between A and C. I don't know about Spot internals, but if the equivalence test is using the same determinization procedure to complement A for the required products, then the bug in the equivalence test is a consequence of the problem in the determinization (i.e., the equiv. test compares the wrong DPA with basically itself), so the issues might be related. It might be useful to know that I found the problem using Spot 2.4.4 and it is still present in the current version 2.5.1. I also attach the smallest automata A, B and C that illustrate the issue and the script I used to search for the counterexample. You can check that: cat aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 0 and autfilt -D -S -p aut_a.hoa | autfilt --accept-word='cycle{!p;p}' -c returns 1. I hope this helps. Thanks and best regards, Anton Pirogov

2 1

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335478点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2229572857咨询
by 傅瑶 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【336248点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2300040163咨询
by 高俏秀 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335418点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2813339771咨询
by 孟荔娜 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【336478点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2810009279咨询
by 邱秋铭 10 Feb '18

10 Feb '18

1 0

哈喽！现邀您注册领取VIP会员和38圆钱实力平台出款安全保障更多优惠尽在【335648点com】天天都有红包雨 VIP周周领工资俸禄月月拿详情企鹅专员2415932228咨询
by 何世 10 Feb '18

10 Feb '18

1 0

Possible Bug in SPOT
by Yong Li 22 Jan '18

22 Jan '18

Hi all, I am using SPOT by following command autfilt --equivalent-to=A.hoa B.hoa to check the equivalence of two Buchi automata A.hoa and B.hoa (attached). It returns nothing and it means two automata are not equivalent. But actually I used GOAL and RABIT to check the equivalence, they said yes. I think you may want to have a look. Regards, Yong -- Yong Li (李勇), State Key Lab. of Computer Science Institute of Software, Chinese Academy of Sciences

2 1

Bug in ltlcross manual
by František Blahoudek 28 Dec '17

28 Dec '17

Hi, I think there is a bug in the manual of ltlcross. There is the paragraph > If the translator produced a Streett or Rabin automaton, these columns > contains the size of a TGBA (or BA) produced by ltlcross from that > Streett or Rabin automaton. Check in_states, in_edges, in_transitions, and in_acc for statistics about the actual input automaton. which seems no longer to be valid as I have no such columns in the output files created by ltlcross v. 2.4.4. Best, Fanda Blahoudek

2 1

genaut --ks-nca error
by Florian Barta 18 Oct '17

18 Oct '17

Hi, when using genaut --ks-nca e.g. genaut --ks-nca=1..10 I get the following error: genaut: print_hoa(): automaton is complete but prop_complete()==false Is this a bug? What can I do to get the desired result? I am using spot version 2.4.1 on Ubuntu 16.04. Best regards, Florian Barta

2 1

is_tt and is_ff in Python bindings
by František Blahoudek 18 Oct '17

18 Oct '17

Hi, I have found out that is_tt and is_ff does nt work as expected in Python. See the attached notebook for details. Best, Fanda Blahoudek

2 1

genaut - documentation
by František Blahoudek 07 Sep '17

07 Sep '17

Hi, there is a tiny inconsistency in man genaut. For the families from Löding's paper there is ... 4N states ... less than n! states. I guess the n and N should share their case. Best, Fanda

2 1

man autcross
by František Blahoudek 06 Sep '17

06 Sep '17

Hi, the manual says in the section DESCRIPTION: The list of automata to use should be supplied on standard input, or using the -f or -F options. However, the tool knows no -f option. Fanda

1 0

can't compile spot
by Pedro Marquez 19 Jul '17

19 Jul '17

I downloaded the spot tar package and tried to compile it using ./configure, make, sudo make install. However, make reports the error: make: *** No targets specified and no makefile found. Stop. and sudo make install reports: make: *** No rule to make target 'install'. Stop. What's happening, what can I do? Thank you in advance, -Pedro Marquez, Prof.

2 1

Swig is required, but isn't
by Clément Gillard 06 Apr '17

06 Apr '17

Hello, I was trying to build Spot on a fresh ArchLinux install, when I came across this issue: > $ ./configure ... > [...] > checking for swig3.0... no > checking for swig... no > [...] > $ make > [...] > swig -c++ -python -py3 -O -nofastproxy -MD -I../buddy/src -MF > .deps/buddy_wrap.TPcxx ./buddy.i > make[3]: swig: Command not found > [...] > make: *** [Makefile:1163: all] Error 2 If Spot requires Swig, shouldn't `configure` fail ? Or, if Swig is only required for users who want to build the Python library, shouldn't the latter not be included in the `all` rule ? If that's any help, I attached my config.log. Regards, -- Clément 'Cigix' Gillard "EAT SLEEP EAT REPEAT" @skrillbug_bot, 2016-06-23

2 1

Reference request: Converting UCW to k-safety automaton
by Ayrat Khalimov 20 Mar '17

20 Mar '17

Hi all, Do you know any tools that can convert universal co-buchi automata into universal safety automata via bounding the number of visits to the final states? (I.e., go to absorbing bad state if visit a final state k times) (Alternatively, convert NBW into nondet finite automaton: accept a word if it visits a final state k times) (I am just trying to avoid work that may have already be done:) Thanks, Ayrat

1 0

Enumerating accepting runs
by Ayrat Khalimov 12 Mar '17

12 Mar '17

hi, Is there a way to get more than one accepting run of the product automaton? Ideally would be to have all simple accepting runs, but some cheap heuristics would also do. I wanted to implement some heuristics [1], but got stuck with the following: how to map edges of the accepting run to the edges of the original product? (or: states of the accepting run to states of the product?) thanks!:) ayrat [1] An heuristics: - get an accepting run, - forbid one edge of that run in the original product (for example, by setting its label to bddfalse), - ask for another accepting run on the thus modified product, - restore that edge and change another edge, and so on.

2 3

underlying algorithm of monitor construction
by Marvin Stenger 03 Mar '17

03 Mar '17

Hello dear spot devs, I need to know which construction is used when I'm translating an LTL formula into a monitor automaton. By that I mean: /spot::formula some_ltl; spot::translator trans;/ /trans.set_type(spot::postprocessor::Monitor) spot::const_twa_graph_ptr aut = trans.run(some_ltl)/ I couldn't find documentation about this, besides some rather informal description. It would be great if you could point me to some more useful documentation about the algorithm or even better a paper on it. Best, Marvin Stenger

2 2

Re: [Spot] c++ help stepping through automaton
by Alexandre Duret-Lutz 06 Dec '16

06 Dec '16

Hi Marvin, > Hello dear spot devs, > > I have a question concerning stepping through an automaton based on the boolean formula assigned to the edge between two states, using c++. > What I want to achieve is the following: > I'm translating an LTL formula into a deterministic monitor automaton, so I have a spot::const_twa_graph_ptr. > Now I simply want to "run" the DFA, i.e., I have a trace and want to perform a state change based on the transition matching the current letter in my trace. > I don't get that step just from the examples or the doxygen documentation. maybe something like unsigned step(const const_twa_graph_ptr& aut, unsigned src, bdd label) { for (auto& edge: aut->out(src)) if (bdd_implies(label, edge.cond)) return edge.dst; throw std::runtime_error("unmatched label"); } > Furthermore it would also be great, if you could tell me how to output the bdd on the edge in an human readable way (boolean formula), as it is done in the online tool of yours (https://spot.lrde.epita.fr/trans.html) I believe this is shown in https://spot.lrde.epita.fr/tut21.html -- Alexandre Duret-Lutz

2 1

Re: [Spot] SPOT installation error
by Alexandre Duret-Lutz 10 Nov '16

10 Nov '16

On Thu, Nov 10, 2016 at 8:44 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: > 2016-11-10 13:01 GMT-06:00 Alexandre Duret-Lutz <adl(a)lrde.epita.fr>: >> On Thu, Nov 10, 2016 at 6:33 PM, ShufangZhu <saffiechu(a)gmail.com> wrote: >> > can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or >> > directory >> > libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a >> > valid libtool archive >> >> Could you show the entire output you get when you type "make" ? > > Please see attached for the entire output. OK, so this error is due to the fact that the source code is in a directory called /home/saffie/LTLf synthesis/spot-2.1.2 with "LTLf synthesis" containing a space. Directory or file names with spaces cannot be supported in Makefiles. Just rename that directory to LTLf_synthesis (or something else), and be sure to run './configure && make clean' (to forget about the old path) before rebuilding with 'make'. -- Alexandre Duret-Lutz

1 0

SPOT installation error
by ShufangZhu 10 Nov '16

10 Nov '16

Hi, I am trying to install SPOT. But after I entered the command "make", there is an error as following, can't read synthesis/spot-2.1.2/buddy/src/libbddx.la: No such file or directory libtool: error: 'synthesis/spot-2.1.2/buddy/src/libbddx.la' is not a valid libtool archive My system is Ubuntu 14.04, 64-bit. And it's a virtual machine. Thanks! Best Regards, Shufang

2 1

Possible Bug (Spot 2.1)
by Reuben Rowe 01 Nov '16

01 Nov '16

Dear Spot Team, I am a postdoc at UCL working on the Cyclist theorem-proving framework, which makes use of Spot. We have recently upgraded Cyclist to use Spot 2.1 from Spot 1.2.4, and one of our benchmark tests has thrown up a possible bug in the Spot library. Cyclist searches for cyclic proofs, and validates them by building two Buchi automata out of a proof and checking language inclusion (ℒ(A) ⊆ ℒ(B)), which we do by first complementing B and then checking emptiness of the product with A. With version 1.2.4, we did this using with the following code: spot::twa a = ...; spot::twa b = ...; spot::tgba_safra_complement complement(&b); spot::tgba_product product(&a, &b); spot::couvreur99_check ec(&product); spot::emptiness_check_result * res = ec.check(); Since version 2.1 does not provide the tgba_safra_complement class, we now use the following code: spot::twa_graph_ptr a = ...; spot::twa_graph_ptr b = ...; spot::twa_graph_ptr det = tgba_determinize(b); spot::twa_graph_ptr complement = to_generalized_buchi(dtwa_complement(det)); spot::const_twa_ptr product = std::make_shared<spot::twa_product>(proof, complement); spot::couvreur99_check ec(product); std::shared_ptr<spot::emptiness_check_result> res = ec.check(); Our benchmark test generates the following automata (given in dot format) for a and b, respectively: digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="0"] 0 -> 1 [label="p_0 & !p_1 & !p_2 & !p_3\n{0}"] 1 [label="S1 t_53"] 1 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 2 [label="S2 t_53,t_49,t_50,t_51,t_52"] 2 -> 2 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 2 -> 3 [label="p_0 & p_1 & !p_2 & !p_3\n{0}"] 3 [label="S3 t_53,t_52"] 3 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 3 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 4 [label="S5 t_53"] 4 -> 4 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 5 [label="S4 t_53"] 5 -> 5 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] } digraph G { rankdir=LR I [label="", style=invis, width=0] I -> 0 0 [label="init"] 0 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3"] 0 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"] 0 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"] 0 -> 4 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 5 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 7 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"] 0 -> 9 [label="p_0 & !p_1 & p_2 & !p_3"] 0 -> 10 [label="p_0 & !p_1 & !p_2 & !p_3"] 0 -> 0 [label="1"] 1 [label="S4,t53"] 1 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 2 [label="S3,t52"] 2 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 3 [label="S3,t53"] 3 -> 1 [label="!p_0 & !p_1 & p_2 & !p_3\n{0}"] 4 [label="S2,t52"] 5 [label="S2,t51"] 5 -> 2 [label="p_0 & p_1 & !p_2 & !p_3"] 6 [label="S2,t50"] 7 [label="S2,t49"] 7 -> 3 [label="p_0 & p_1 & !p_2 & !p_3"] 8 [label="S2,t53"] 8 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 8 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 9 [label="S5,t53"] 9 -> 9 [label="p_0 & !p_1 & p_2 & !p_3\n{0}"] 10 [label="S1,t53"] 10 -> 6 [label="!p_0 & p_1 & !p_2 & !p_3\n{0}"] 10 -> 8 [label="!p_0 & p_1 & !p_2 & !p_3"] } The code I gave above returns a non-null (i.e. non-empty) result, however we expect that this should actually return an empty result. What I have discovered is that the code above does indeed return an empty result when the use_simulation flag to the tgba_determinize function is set to false (the values of the other two flags do not make a difference). Thus, it seems to me that this is a bug, no? I am happy to provide any more information which is necessary for diagnosis. Best wishes, Reuben Rowe.

2 2

[SPOT Question] Little Question about LTL/PSL Fragment
by Willy Chang 05 Sep '16

05 Sep '16

Hello, I'm a graduate student at National Taiwan University (Taiwan), doing automatic verification related researches. Currently I'm working on integration of PSL translation with other types of Büchi automata and formats with our own tool (based on Java), which the linear fragment part is implemented by Spot (and ltl2tgba). I appreciate this fantastic tool and all of your respectable work on this. Upon using ltl2tgba, I'd like to ask some basic question regarding F formula and SERE sequences. Take the following formula as example: G ( {a;b} -> F q ) where a, b, q are all atomic Boolean expressions. ltl2tgba would give me the result like the following: https://spot.lrde.epita.fr/spotimg/af005ecb477ea78d3b55f538089ac0fce1fa99f7… (This is captured from online Spot converter, but is the same as one output by command-line tools.) As we can see, there are multiple transitions marked as "a & !q", meaning this automaton is a non-deterministic one. Is this intended to be so? If yes, how could I specify Spot to get a deterministic output? If no, would this be a bug or something ambiguous? Also, I have been curious about the algorithm that Spot parses PSL fragment. It seems like Spot first extracts PSL symbols to LTL compatible ones and then apply LTL translation method to automata, Is this right? Or did I miss some parts? I'm new to PSL translations and reading related papers now (thanks for the SPOT citation page). Please feel free to correct me or recommend me some must-read publications. Currently I"m working on the IEEE Standard (2010) and the book Practical Introduction to PSL. Thank you very much. Sincerely, Willy Chang Dept. of Information Management National Taiwan University

2 1

ltl2dstar
by armin mojoodi 13 Jul '16

13 Jul '16

Hello I want to use ltl2dstar.exe for a project, but I have a problem with v.0.5.3. when I run it with cmd it returns an error... Exception in file common/RunProgram.win32.cpp at line 85: CreateProcess failed... I would be appreciate if you tell me how should I fix it. Best, Armin

2 1

Online translator: RuntimeError for LTL3BA
by Ayrat 07 Jul '16

07 Jul '16

hi there, smth is wrong with online translator for LTL3BA -- see message below. Thanks for amazing web-page! regards, ayrat *RuntimeError* Python 3.4.2: /usr/bin/python3 Thu Jul 7 11:57:15 2016 A problem occurred in a Python script. Here is the sequence of function calls leading up to the error, in the order they occurred. /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in **() 747 dont_run_dot = print_stats(degen, True) 748 automaton.set_name(str(f)) => 749 render_automaton(degen, dont_run_dot) 750 degen = 0 751 automaton = 0 *render_automaton* = <function render_automaton>, *degen* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, *dont_run_dot* = False /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *render_automaton*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, dont_run_dot=False) 314 else: # TGBA 315 if not dont_run_dot: => 316 hoaname = save_hoa(automaton) 317 spot.print_dot(dotsrc, automaton, '.t' if buchi_type == 't' else '.') 318 render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname) *hoaname* = None, /global/ *save_hoa* = <function save_hoa>, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> > /var/www/html/cgi-bin/spotcgi.py <file:///var/www/html/cgi-bin/spotcgi.py> in *save_hoa*(automaton=<spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >) 259 def save_hoa(automaton): 260 hoasrc = spot.ostringstream() => 261 spot.print_hoa(hoasrc, automaton, 't' if buchi_type == 't' else '') 262 hoasrc = hoasrc.str() 263 hoasrc += '\n' /global/ *spot* = <module 'spot' from '/usr/lib/python3/dist-packages/spot/__init__.py'>, spot.*print_hoa* = <built-in function print_hoa>, *hoasrc* = <spot.impl.ostringstream; proxy of <Swig Object of type 'std::ostringstream *' at 0x7f2ae4164d20> >, *automaton* = <spot.impl.twa_graph; proxy of <Swig Object of t...ed_ptr< spot::twa_graph > *' at 0x7f2ae4164810> >, /global/ *buchi_type* = 't' *RuntimeError*: print_hoa(): automaton uses unregistered atomic propositions args = ('print_hoa(): automaton uses unregistered atomic propositions',) with_traceback = <built-in method with_traceback of RuntimeError object>

3 2

Java Implementation
by Виктор Фридман 11 Jun '16

11 Jun '16

Hello! Do You have any Java implementations of Spot? Regards. Отправлено из Почты для Windows 10

2 1

Completing automata using efficiente bdd operations
by Sergio Hernández 23 May '16

23 May '16

Hi, i would like to ask you about the most efficient way of completing an automaton using bdd operations. we are working with huge automata and we want to improve the automaton creation process. For that, one of the bottlenecks is generating the logical formulas corresponding to the automaton transitions as bdds. For example, let us consider we have the following automaton: State 0 | | a & b | v State 1 | | a & c | v State 2 Then, the alphabet is {a,b,c,d,e}. Thus, we need to add (!c & !d & !e) to the first transition and (!b & !d & !e) to the second one in order to make queries such as "F(e)". Currently, we are implementing this manually using a loop where for each transition we add the negation of every condition that is not present in the transition. But it is not fast enough. Is there any bdd operation to implement this in an efficient way? Thanks in advance, Sergio Hernández

2 1

Acceptance check in Spot
by Matthias Heizmann 14 Mar '16

14 Mar '16

Hi Spot developers, I just extended our automata library https://ultimate.informatik.uni-freiburg.de/?ui=int&tool=automata_script_in… with support to write Büchi automata in the HOA format. Now, I just wanted to check a few results without implementing support to read HOA files. Syntactically my files seem to be correct, (example attached, file is read by Spot), but I also wanted to do some semantic check, e.g., test if a certain word is accepted. Spot provides quite a number of sophisticated operations but I did not find something "simple" like an acceptance check. Have I overlooked it or is it not documented? For my purpose it is sufficient if it works on the "usual" Büchi automata. Best, Matthias

2 3

Creating bdds
by Miriam Blank 10 Jan '16

10 Jan '16

Hi, Can you please explain the api for creating a bdd? How can I create a bdd? How do I define it? How do I give parameter names so that I can later use it to model check a formula? What is the meaning of bdd_ithvar and bdd_nithvar and the int parameter they receive? I would be very happy if you can supply a simple example. Thank you very much and happy new year, Miriam

2 5

Parsing HOA using Python
by Marcel Walter 10 Jan '16

10 Jan '16

Hi all, I am a masters student of computer science at University of Bremen, Germany. I am working with Büchi-Automata for a study at the moment. Therefore I want to parse an HOA file representing a Büchi-Automaton using Python. It would be great to get an object in Python representing the automaton. So that I can iterate over the states and their edges, read the labels, etc. Can this be done using Spot? If so, how? It would be nice to have a code example. Thank you so much for your help! Best regards from Germany, Marcel Walter

2 2

Python documentation for spot
by Miriam Blank 17 Nov '15

17 Nov '15

Hello, Is there a full documentation of the python api for spot? All I found are the examples in wrap/python/tests. Thank you, Miriam

2 1

Unambiguous test on empty automata
by Ming-Hsien Tsai 20 Oct '15

20 Oct '15

Dear Spot developers, Attached is an automaton accepting an empty language. I think it is supposed to be unambiguous. But when I ran the following command, I got 0. autfilt --count --is-unambiguous empty.hoa After tracing the code, I found that the problem might be caused by get_init_state_number (called in the product function), which creates a new state if the input automaton has no state. -- Ming-Hsien

2 1

SPOT error in make check
by Christopher Ziegler 24 Aug '15

24 Aug '15

Hello Ladies and Gentlemen, I used your program (SPOT) on Ubuntu 12.4. 32bit, configured it with the two parameters --disable-python and --prefix=/home/my_username (for which I don't need any sudo priviliges to read/write. Then I did make check and the program reported the following: See src/tests/test-suite.log Please report to spot(a)lrde.epita.fr However, I ran make install afterwards, and tried the program and it seems to work. But when I tried to do the same (last week or so), I didn't use the --prefix parameter and I got an error, when I tried to start the program: it said: "error while loading shared libraries: libspot.so.0: cannot open shared object file: No such file or directory" I also include the src/tests/test-suite.log in the attachment. I hope this helps you finding a bug or something. Since the program works for me now, I just wrote you because it said "Please report to spot@..." . If you need more information (for example, which compiler I used etc.) you can write me back. Regards, Christopher Ziegler

2 2

Bug Report
by Oscar Chang 05 Aug '15

05 Aug '15

If you enter (FGa)||(FGb) and tick the option for the degeneralized buchi automaton, it still gives a generalised one.

2 1

Installation of SPOT 1.99.1
by Vitus Lam 30 Jun '15

30 Jun '15

Dear Alexandre, I tried to install SPOT 1.99.1 on Fedora 21. During the execution of the "make" command, the following error returned. How can I fix the compilation issue? make[3]: Entering directory '/home/vituslam/spot-1.99.1/wrap/python' Making all in . make[4]: Entering directory '/home/vituslam/spot-1.99.1/wrap/python' /bin/sh ../../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I../.. -I/usr/include/python3.4m -I../../src -I../../src -I../../buddy/src -DSWIG_TYPE_TABLE=spot -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++11 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT spot_impl_wrap.lo -MD -MP -MF .deps/spot_impl_wrap.Tpo -c -o spot_impl_wrap.lo `test -f './spot_impl_wrap.cxx' || echo './'`./spot_impl_wrap.cxx libtool: compile: g++ -DHAVE_CONFIG_H -I. -I../.. -I/usr/include/python3.4m -I../../src -I../../src -I../../buddy/src -DSWIG_TYPE_TABLE=spot -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++11 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT spot_impl_wrap.lo -MD -MP -MF .deps/spot_impl_wrap.Tpo -c ./spot_impl_wrap.cxx -fPIC -DPIC -o .libs/spot_impl_wrap.o ./spot_impl_wrap.cxx:155:21: fatal error: Python.h: No such file or directory # include <Python.h> ^ compilation terminated. Makefile:1282: recipe for target 'spot_impl_wrap.lo' failed make[4]: *** [spot_impl_wrap.lo] Error 1 make[4]: Leaving directory '/home/vituslam/spot-1.99.1/wrap/python' Makefile:1349: recipe for target 'all-recursive' failed make[3]: *** [all-recursive] Error 1 make[3]: Leaving directory '/home/vituslam/spot-1.99.1/wrap/python' Makefile:1107: recipe for target 'all-recursive' failed make[2]: *** [all-recursive] Error 1 make[2]: Leaving directory '/home/vituslam/spot-1.99.1/wrap' Makefile:1186: recipe for target 'all-recursive' failed make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory '/home/vituslam/spot-1.99.1' Makefile:1109: recipe for target 'all' failed make: *** [all] Error 2 Thanks in advance for your assistance. Vitus Lam

2 3

Multiple (all) accessing runs
by Ulrich Kühne 29 Jun '15

29 Jun '15

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Hi, I have implemented a simple LTL model checker in c++ using SPOT. For a failing property, I can get a counterexample using the method accepting_run() on the emptiness_check_result. Now I am interested in all accepting runs, or, more precisely in all the states that are part of the prefix of some accepting run. What would be the best SPOTish way to obtain these? I would be fine with the runs and find the relevant states myself. Thanks for any suggestion. Regards, Ulrich -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.22 (GNU/Linux) iQEcBAEBAgAGBQJVjAUTAAoJEM0dHSf/6N1YGtEH/R5szUBeK0WfWKCULAiv3Q2P MKD+AaEsZM0g6ujWLNRzVUnh5DA5WmlzmbFTPPDKEKNtaPO6sKv7ydLfsfh2GWJX I+tsM7Uzf94hTIuwY9uTAdtSpQIWGflhr3Q6ncV77KEYgaHGFPB0Zg2BaUYtgVZ+ zgglBCowJHoEbj13tX9LlPOLGyzD95TZ8LCG1CBtLwtoy1h/x4jFjB4vEIlXGeyw q2uEUjF9oz9thA4x/NW8X39s9E/UIi62wZb2nuLK+a8QO5FX3cJQWe4PBZ7fl42m L8kNEeLEvZ5sH7eznkk/XiHtf/fdB+85DDq/dB8lF335lgt2ES66rvxXk6TRFRM= =d4aZ -----END PGP SIGNATURE-----

2 1

[Bugreport] libspotltsmin is not installed
by Colange Maximilien 29 Jun '15

29 Jun '15

Hi, I tested the new version of Spot. The libspotltsmin is marked as "noinst" in the Makefile.am, and thus does not install when running make install. In previous versions, libspotdve2 was installed, so I suppose it is a bug. Side note: this new version is nice (especially the smart pointers). Yet, the documentation for accepting conditions API is incomplete, but I guess it is on the TODO list for the 2.0. -- Maximilien Colange CUI Université de Genève Battelle Bâtiment A route de Drize 7 1227 Carouge SWITZERLAND Tel: +41 22 379 01 73

2 2

Checkpn
by Alexandre Duret-Lutz 24 Jun '15

24 Jun '15

Hi Kerrache, Kerrach Massipssa wrote: > I would to ask you a question about Checkpn. > I compiled Spot (last version) and for Checkpn I do it like this : > ./configure --with-spot=/usr/local/ > > And for make I get an error in main.cpp at this ligne > spot::ltl::formula* f = spot::ltl::parse(ltl_string, pel); > In fact I just add const to correct the error. But i get > another error which i don't understand : > /usr/local//include/spot/tgbaalgos/reachiter.hh:102: > undefined reference to `spot::tgba_reachable_iterator::~tgba_reachable_iterator()' > > Could you help me to solve the problem ? And thank you in advance for response. CheckPN is not working with any recent version of Spot, and not really maintained. The issue is tracked at https://gitlab.lrde.epita.fr/spot/spot/issues/19 If you really need it and are unable to fix it, I think your best bet is use older versions of Spot :-( -- Alexandre Duret-Lutz

1 0

LTL operator precedence
by Molnár Vince 08 Jun '15

08 Jun '15

Dear SPOT Developers, I am writing to you to ask what the operator precedence is that you use for parsing LTL formulae. As I use SPOT to translate LTL formulae to automata, but I also need to handle expressions separately, it would be crucial to stay compatible with your implementation. I am working on .NET, so I cannot simply use your library as a parser and AST metamodel. Thank you for your time! Best regards, Vince Molnár

2 1

LTL input format in SPOT
by Jianwen Li 02 Mar '15

02 Mar '15

Dear Alexandre: I am trying to figure out whether SPOT can accept boolean assertions such as "x >1". For example, can SPOT recognize the LTL formula F (x > 1), which is accepted by Promela format? I tried it with SPOT by ./ltl2tgba -f "F (x>1)" and SPOT fails to parse it. But I really want to make sure whether I have used it correctly. Many thanks~ -- Best Regards Jianwen Li

2 1

Negation Propagation using Spot library
by Dennis Park 18 Oct '14

18 Oct '14

Hello, My name is Dennis Park and I'm a student at the University of British Columbia. I am using the Spot library in a research project I am currently working on and I wanted to ask whether the Spot library supports negation propagation. More specifically, I would like to take an ltl formula spot::ltl::formula* f and propagate all negations in f so that negations only occur before atomic propositions. Does the Spot library support such a functionality? If so, where in the documentation could I find information on it (I tried to look for something like it in the documentation but had trouble finding anything). Thank you, Dennis Park

2 1

Question sur la simplification de formules LTL
by Amélie DAVID 14 Oct '14

14 Oct '14

Bonjour, Je suis en doctorat d'informatique à l'université d'Evry et je travaille sur la logique ATL. Je viens de découvrir votre outil Spot et en particulier l'outil de simplification des formules. Je suis entrain de développer des méthodes de tableaux pour ATL, et je souhaiterais également pouvoir simplifier les formules fournies en entrée de l'outil. J'aurais donc voulu savoir s'il existait une référence dans la littérature ou une compilation de l'ensemble (ou en tout cas la majorité) de ces simplifications. J'ai beau chercher depuis un petit moment et je n'ai rien trouvé à l'exception de votre outil Spot. Merci d'avance pour l'aide que vous pourriez m'apporter concernant cette question. Bien cordialement, Amélie DAVID

2 1

I'd like to add you to my professional network on LinkedIn
by Jianwen Li 23 Sep '14

23 Sep '14

Hi, I'd like to add you to my professional network on LinkedIn. - Jianwen Accept: http://www.linkedin.com/blink?simpleRedirect=czgSdPsUcjsSdP4Zh4BKrSBQonhFtC… You received an invitation to connect. LinkedIn will use your email address to make suggestions to our members in features like People You May Know. Unsubscribe here: http://www.linkedin.com/blink?simpleRedirect=79Chj8BonhFs6l5cylBp79Ic3gBt6Z… Learn why we included this at the following link: http://www.linkedin.com/blink?simpleRedirect=e3wTd3RAimlIoSBQsC4Ct7dBtmtvpn… © 2014, LinkedIn Corporation. 2029 Stierlin Ct. Mountain View, CA 94043, USA

1 0

[LTL2TGBA] SPOT translation produces unexpected results
by Caroline Lemieux 13 Aug '14

13 Aug '14

Hello, I'm an undergraduate student at UBC working on a log analysis project under Ivan Beschastnikh <http://www.cs.ubc.ca/~bestchai/>. I'm using SPOT in the project to parse LTL strings into formulae, and now trying to use the translation to automata functionality. The situation I'm dealing with would involve passing a finite sequence of states into the automaton, and the description of the Monitor output appeared to be what I needed. However, the monitor DFA provided for the response formula G(a->Fb) was an all-accepting DFA: which didn't seem to align with the given definition of monitor. I've been searching the documentation, but can't find anything more describing why this DFA would be produced. I've also been looking for a description of acceptance condition syntax, especially for the state-based degeneralized Buchi automaton, where both edges and states are labeled as accepting. Could you direct me to any documentation on these subjects or give any insight on why the above monitor is being produced for the response pattern? (As defined by the specification pattern project here <http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml>.) Merci, Caroline Lemieux

2 1

Invitation to connect on LinkedIn
by Jianwen Li 30 Oct '13

30 Oct '13

LinkedIn ------------ I'd like to add you to my professional network on LinkedIn. - Jianwen Jianwen Li Student at 华东师范大学 Shanghai City, China Confirm that you know Jianwen Li: https://www.linkedin.com/e/-nsg3vs-hndxc2hn-6m/isd/17671877642/tb7AAFae/?hs… -- You are receiving Invitation to Connect emails. Click to unsubscribe: http://www.linkedin.com/e/-nsg3vs-hndxc2hn-6m/u-a3zDAksnebW94Ku3oUMPGzZndMu… (c) 2012 LinkedIn Corporation. 2029 Stierlin Ct, Mountain View, CA 94043, USA.

1 0

monitor construction error
by Angelo Gargantini 06 Mar '13

06 Mar '13

Dear spot maintainers, we have been using SPOT by using its web site to build monitors from LTL formulas (http://spot.lip6.fr/ltl2tgba.html) Now with the new version, translation to monitors gives always an error like: ome maps are not empty Variable Map: 0 Free 1 Var[a] x1 { 0xa001d10 } Anonymous lists: [0] Free list: (0, 1) close failed in file object destructor: sys.excepthook is missing lost sys.stderr Could you please fix it? Thanks Angelo Gargantini University of Bergamo Italy

2 2

check for the emptyness of the automata
by Jianwen Li 08 Dec '12

08 Dec '12

Dear Sir: I want to ask whether SPOT integrate some algorithm that can check the generated autoamta's emptyness ? Recently I want to use SPOT to do the LTL satisfiability checking. If you do not, I have to combine SPOT with SPIN to achieve that. Thanks very much! -- Best Regards Jianwen

2 1

Re: [Spot] TGBA Doubt
by Alexandre Duret-Lutz 20 Jun '12

20 Jun '12

On Tue, Jun 19, 2012 at 11:48 AM, Agrawal, Akshay <akshay.agrawal(a)vanderbilt.edu> wrote: > Dear Alexandre, > Thank you for a prompt reply. So I think my perception was wrong > about TGBA. I did not learn about TGBA from SPOT's wiki. I learnt it > from some papers and Wikipedia. But I think I formed a wrong > impression. > So after your explanation I believe that a TGBA for G(p->Xr) is a > special case of TGBA with all transitions as accepting transitions?? Yes. Any safety formula can be translated into a TGBA without acceptance set. > Also, there was a need for me to convert these TGBA generated from > SPOT to C code so I wanted to know how is Acc[r] logically read?? > Because sometimes in complex TGBA's there are various such accepting > sets where we may have Acc[r] and Acc[r|q] or something. So the > Boolean condition in the brackets of Acc[] , how is it read/what > does it exactly mean?? I think this will help me to get C code out > of these TGBAs. You should regard these just as unique strings used to name the acceptance conditions. They could be numbers, it would not change the language. When evaluating an ω-word on such an automaton, you want to see each of these strings infinitely often. The fact that they denote subformulae is an implementation detail of Spot's translation. During the translation of LTL into TGBA, the string actually denotes subformulae that have been promised to hold eventually. (The transitions that don't have Acc[φ] are the transitions that promise to see φ later/) See http://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf if you want more details. However you may not rely on this second meaning, because some post-processing (like degeneralization, WDBA-minimization) might introduce Acc[1]. This Acc[1] is also used during PSL translation. Obviously it makes not sense to promise "true", since it's always true :-) If you are confused, just forget about the previous two paragraphs. Unless you want to change the translation algorithm, there is no need to know what the argument of Acc[] means. > Does SPOT give a C code or other type of executable monitor type > code for generated TGBAs?? Spot does not generate C. What we call monitor (in Spot at least) is a finite automaton that accepts all finite prefixes of the executions that satisfy some formula. Spot can generate a deterministic monitor for any LTL formula, and will present it as a TGBA without acceptance condition. See the "monitor" output on the online translator. -- Alexandre Duret-Lutz

1 0

how to add new features to spot
by 李建文 19 Jun '12

19 Jun '12

Dear sir: I am trying to extend spot by adding a new ltl-to-ba translation algorithm. The brief idea is that I extend the formula structure in spot so that I can use the parser for ltl formulas. Now I have finished the code and want to compile my codes with those in spot, but I am confused how I can achieve this. Does spot provides some interfaces that can help someone to extend it? Thanks very much for attention and I am expecting your reply. Best Jianwen

2 4

TGBA Doubt
by Agrawal, Akshay 19 Jun '12

19 Jun '12

Hi, I am a Grad Student at Vanderbilt University,TN,USA and am working on formal verification of software systems. I was using spot library and your site and wanted to know : if a TGBA ( Transition based generalized Buchi automaton) has all transitions as accepting transitions by definition then what is this {ACC[r]} condition that explicitly appears ion automaton when I write LTL formula : F r. And why don't I get any such thing when I use LTL formula : X r. I will appreciate your reply. Thanks in advance, Akshay Agrawal

2 1