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