8 Mar
2017
8 Mar
'17
2:26 p.m.
(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(a)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