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