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
Good afternoon,
I am Jueming, a Ph. D. student at Arizona State University. I would like to
use spot for my research, such as getting the graph of an LTL formula.
I downloaded 'linux-64/spot-2.9.6-py38_2.tar.bz2' and ran 'conda install -c
adl spot' within the extracted folder. 'spot 2.5.2' is shown in conda list
and also in python packages. However, 'import spot' doesn't work. The error
says, 'No module named 'spot''.
I have also tried 'linux-64/spot-2.9.4-py38_2.tar.bz2', 'conda install -c
adl/label/adl spot', 'conda install -c adl/label/dev spot', append system
path before import spot, and export LD_LIBRARY_PATH. But spot still doesn't
work on my pc.
Could you please help me install spot?
Thanks in advance and looking forward to hearing from you.
Best,
Jueming
