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