(may be someone else would need this) For now I ended up parsing the result of `spot.bdd_format_set` which nicely prints things like <cancel:0, grant:0, req:0, go:0><cancel:1, grant:0, req:1, go:0> (bdd as a set of cubes enclosed in <>) ( the formula was (!cancel & !grant & !reg & !go) | (cancel & !grant & reg & !go) ) (if there is a better way -- write:) thanks, Ayrat On Wed, Mar 8, 2017 at 11:32 AM, Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
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