hi!
With the aid of SPOT I am developing a counter-example guided synthesizer
in python. See [1] if interested for details.
My question is:
I am trying to parse twa_run in python,
namely, parse the labels of the each step (`spot.impl.step`).
Is there a python way to walk through BDD?
(The label is a simple cube expressed in BDD, and I need to convert it into
my internal structure)
(yes, this is rather a question about python interface for buddy)
(no, that is not feature request:) if not possible, I will simply print the
label and parse the string, that is not crucial)
[1]
The idea is
- guess the model,
- then model check it and get a counter-example
- then encode the counter-example into the "guesser" (which uses an SMT
solver)
thanks,
Ayrat
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
===============================
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
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.
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.
