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