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
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
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
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
Dear Spot developers,
I am Yong Li, a Phd student from Chinese Academy of Sciences.
I am writing to you to ask an implementation question about the
translation from LTLf to NBAs in Spot.
currently if I use following command line:
ltlfilt --from-ltlf -f "((G((P83) -> (X((P145)) | X(X((P145))) |
X(X(X((P145)))) ))) -> ( G((P21) -> (X( (P118) | (P83)) | X(X(
(P118) | (P83))) | X(X(X((P118) | (P83)))) )) & G( (P118) ->
X(!(P118))) & G( (P83) -> X(!(P118) U (P145)))))" | ltl2tgba | autfilt
--remove-ap=alive --small -B
I was able to get a weak DBA with only 8 states.
However, if I use following c++ code to do the same job:
auto pf1 = spot::parse_infix_psl(argv[1]);
if (pf1.format_errors(std::cerr))
{
std::cerr << "error: " << argv[1] << std::endl;
return -1;
}
// formula
auto f1 = pf1.f;
std::cout << f1 << std::endl;
// translate to ltlf
//auto ltlf = spot::from_ltlf(f1, "alive");
spot::translator trans;
trans.set_type(spot::postprocessor::BA);
trans.set_pref(spot::postprocessor::Small);
trans.set_level(spot::postprocessor::High);
spot::twa_graph_ptr aut = trans.run(spot::from_ltlf(pf1.f));
spot::remove_ap rem;
rem.add_ap("alive");
aut = rem.strip(aut);
spot::postprocessor post;
post.set_type(spot::postprocessor::BA);
post.set_pref(spot::postprocessor::Small); // or ::Deterministic
post.set_pref(spot::postprocessor::High); // or ::Deterministic
aut = post.run(aut);
I would get a DBA with 16 states, which has much more states than the
one from the command line.
The full source code is attached to this email.
Could you tell me how I can change the code above so to get the same DBA
from the command line?
Thank you very much.
BTW: I would like to appreciate the Spot tool which is a tool I would
install on my every Ubuntu system.
Yong
Dear Spot team,
I've tried to pull docker image using command "sudo docker pull
registry.lrde.epita.fr/spot-sandbox", however, I got the following response:
"Unable to find image 'registry.lrde.epita.fr/spot-sandbox:latest' locally
docker: Error response from daemon: error parsing HTTP 403 response body:
invalid character '<' looking for beginning of value: "<!DOCTYPE HTML
PUBLIC \"-//IETF//DTD HTML 2.0//EN\">\n<html><head>\n<title>403
Forbidden</title>\n</head><body>\n<h1>Forbidden</h1>\n<p>You don't have
permission to access /v2/spot-sandbox/manifests/latest\non this server.<br
/>\n</p>\n</body></html>\n".
See 'docker run --help'."
, any insight would be appreciated.
Best regards,
Jiraphapa J.
Dear 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.
Dear Alexandre and Guillermo,
We tried to link Spot statically - Alexandre's suggestion did not quite work for us, but Danil had worked out a different method, see below.
Regards,
Victor.
------------------------
Hi Victor,
This looks much simpler than the way I figured out by try and error:
https://workcraft.org/devel/backend/spot
However the binaries are still dynamically linked after this:
~/spot/bin$ ldd ltl2tgba
linux-vdso.so.1 => (0x00007fff6c9f8000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6
(0x00007fe09b967000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fe09b65e000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1
(0x00007fe09b446000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fe09b07c000)
/lib64/ld-linux-x86-64.so.2 (0x00007fe09bcf3000)
I think I will stick for what is working for us rather than trying to understand what goes wrong with these --disable-shared and --enable-static flags...
Maybe we should share our experience with Guillermo and also let Spot team know about the issue?
Cheers,
Danil
> -----Original Message-----
> From: Spot <spot-bounces(a)lrde.epita.fr> On Behalf Of Alexandre Duret-
> Lutz
> Sent: Tuesday, May 21, 2019 9:06 AM
> To: Guillermo Perez <gaperez64(a)gmail.com>
> Cc: spot <spot(a)lrde.epita.fr>; Guillermo A. Pérez
> <guillermoalberto.perez(a)uantwerpen.be>
> Subject: Re: [Spot] ltlsynt light
>
> On Tue, May 21, 2019 at 9:47 AM Guillermo Perez <gaperez64(a)gmail.com>
> wrote:
> >
> > Hello,
> >
> > I am part of the SYNTCOMP organization team this year. Ltlsynt seems
> > to me the easiest tool to migrate into the, new this year, StarExec
> > competition architecture. However, while trying to prepare a binary, I
> > found that spot generates 1. a .libs folder with libraries 2. very
> > large dependencies like libspot.so
> >
> > Is there a way to generate a statically-liked ltlsynt binary with no
> > hidden dependencies and without all of spot in a dynamically-liked
> > file? (E.g. an option like "make ltlsynt" would be ideal.)
>
> Hi Guillarmo,
>
> Like any libtool-based project, you can generate a statically-linked version
> of the Spot binaries with
>
> ./configure --disable-shared --enable-static make -j4
>
> (don't forget to run "make clean" first if you are doing this on a previous
> build)
>
> --
> Alexandre Duret-Lutz
> _______________________________________________
> Spot mailing list
> Spot(a)lrde.epita.fr
> https://lists.lrde.epita.fr/listinfo/spot
Hello,
I am part of the SYNTCOMP organization team this year. Ltlsynt seems to me
the easiest tool to migrate into the, new this year, StarExec competition
architecture. However, while trying to prepare a binary, I found that spot
generates
1. a .libs folder with libraries
2. very large dependencies like libspot.so
Is there a way to generate a statically-liked ltlsynt binary with no hidden
dependencies and without all of spot in a dynamically-liked file? (E.g. an
option like "make ltlsynt" would be ideal.)
Best,
Guillermo A. Perez
Hi Alexandre,
> Meanwhile, I have implemented SVA's first_match and ##[i:j].
>
> The latter is just syntactic sugar:
> a ##[i:j] b = a:([*i:j];b)
> ##[i:j] b = [*i:j];b
> ##i = ##[i:i]
While you are at this, maybe you could also implement SVA's ##[*] and ##[+] (as sugar for ##[0:$] and ##[1:$]) for completeness?
Please also note that the equality a ##[i:j] b = a:([*i:j];b) is wrong (despite being recommended in some textbooks!), e.g.
{empty_word} ##[0:1] {a} =[by definition] = ({empty_word} ##0 {a}) | ({empty_word} ##1 {a}) = {} | {a} = {a}
but
{empty_word} : ([*0:1];{a}) = {}
The reason is that ##0 always loses the empty word. Hence, it's best to split off ##0 (fusion) from ##[i>0:j] (union of concatenations) and handle them separately.
Regards,
Victor.
