Walking through BDD formula in python
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
(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
Hi Ayrat, On Wed, Mar 8, 2017 at 11:32 AM, Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
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)
You can iterate through a BDD with BuDDy as follows:
import spot import buddy run = spot.translate('a & !b').accepting_run() print(run) Prefix: 1 | a & !b Cycle: 0 | 1 {0}
b = run.prefix[0].label print(type(b)) <class 'buddy.bdd'> # let's make sure that b is a cube # (depending on how the run was generated you might not need that) c = buddy.bdd_satone(b) # iterate on all variables of a cube assert c != buddy.bddfalse res = [] while c != buddy.bddtrue: ... var = buddy.bdd_var(c) ... h = buddy.bdd_high(c) ... if h == buddy.bddfalse: ... res.append(-var) ... c = buddy.bdd_low(c) ... else: ... res.append(var) ... c = h ... print(res) [0, -1]
Unfortunately, you'll only get variable numbers instead of the actual propositions. The mapping between atomic propositions and BDD variables is done by the spot.bdd_dict instance returned by run.aut.get_dict(), unfortunately this class does not seem to be completely binded in Python so far, and I'm not overly excited to expose it too much in its current state. However another way to get the mapping between atomic proposition and BDD variables is to pretend that you register the variables again:
for i in run.aut.ap(): ... print(i, run.aut.register_ap(i)) a 0 b 1
So now you can decode [0, -1] as meaning a&!b.
(no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial)
In fact the C++ library as a function called spot::bdd_to_formula that would be much cleaner to use. Unfortunately it is not yet binded in Python. I'll make it available in the next release. With this function we can explore boolean labels using the LTL formula interface:
import spot run = spot.translate('a & !b').accepting_run() b = run.prefix[0].label f = spot.bdd_to_formula(b, run.aut.get_dict()) f a & !b f._is(spot.op_And) True len(f) 2 f[0] a f[0]._is(spot.op_ap) True f[1] !b f[1]._is(spot.op_Not) True f[1][0] b
(the above will only work in the next release) -- Alexandre Duret-Lutz
A follow up question (related to those old ones): Is it possible to enumerate all cubes of the 'transition condition'? (in C++) That is, given a BDD corresponding of a transition condition, enumerate all its conjuncts: for instance, if the formula of the transition condition is equivalent to (a & b) | (a & c) | (x & !y) then enumerate these conjuncts, one by one: - a & b, - a & c, - x & !y. It seems that I could traverse the transition condition formula, but not sure if it is always in the DNF form, etc. thanks, and have a nice day, Ayrat On Wed, Mar 8, 2017 at 2:36 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
Hi Ayrat,
On Wed, Mar 8, 2017 at 11:32 AM, Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
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)
You can iterate through a BDD with BuDDy as follows:
import spot import buddy run = spot.translate('a & !b').accepting_run() print(run) Prefix: 1 | a & !b Cycle: 0 | 1 {0}
b = run.prefix[0].label print(type(b)) <class 'buddy.bdd'> # let's make sure that b is a cube # (depending on how the run was generated you might not need that) c = buddy.bdd_satone(b) # iterate on all variables of a cube assert c != buddy.bddfalse res = [] while c != buddy.bddtrue: ... var = buddy.bdd_var(c) ... h = buddy.bdd_high(c) ... if h == buddy.bddfalse: ... res.append(-var) ... c = buddy.bdd_low(c) ... else: ... res.append(var) ... c = h ... print(res) [0, -1]
Unfortunately, you'll only get variable numbers instead of the actual propositions.
The mapping between atomic propositions and BDD variables is done by the spot.bdd_dict instance returned by run.aut.get_dict(), unfortunately this class does not seem to be completely binded in Python so far, and I'm not overly excited to expose it too much in its current state.
However another way to get the mapping between atomic proposition and BDD variables is to pretend that you register the variables again:
for i in run.aut.ap(): ... print(i, run.aut.register_ap(i)) a 0 b 1
So now you can decode [0, -1] as meaning a&!b.
(no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial)
In fact the C++ library as a function called spot::bdd_to_formula that would be much cleaner to use. Unfortunately it is not yet binded in Python. I'll make it available in the next release. With this function we can explore boolean labels using the LTL formula interface:
import spot run = spot.translate('a & !b').accepting_run() b = run.prefix[0].label f = spot.bdd_to_formula(b, run.aut.get_dict()) f a & !b f._is(spot.op_And) True len(f) 2 f[0] a f[0]._is(spot.op_ap) True f[1] !b f[1]._is(spot.op_Not) True f[1][0] b
(the above will only work in the next release) -- Alexandre Duret-Lutz
O, found the answer. According to the implementation of the function spot::bdd_to_formula, any formula of transition.cond is of the form of "sum of products", so a straightforward traversing of the formula bdd_to_formula(transition.cond) is sufficient. On Wed, May 26, 2021 at 2:30 PM Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
A follow up question (related to those old ones):
Is it possible to enumerate all cubes of the 'transition condition'? (in C++) That is, given a BDD corresponding of a transition condition, enumerate all its conjuncts: for instance, if the formula of the transition condition is equivalent to (a & b) | (a & c) | (x & !y) then enumerate these conjuncts, one by one: - a & b, - a & c, - x & !y.
It seems that I could traverse the transition condition formula, but not sure if it is always in the DNF form, etc.
thanks, and have a nice day, Ayrat
On Wed, Mar 8, 2017 at 2:36 PM Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
Hi Ayrat,
On Wed, Mar 8, 2017 at 11:32 AM, Ayrat Khalimov <ayrat.khalimov@gmail.com> wrote:
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)
You can iterate through a BDD with BuDDy as follows:
import spot import buddy run = spot.translate('a & !b').accepting_run() print(run) Prefix: 1 | a & !b Cycle: 0 | 1 {0}
b = run.prefix[0].label print(type(b)) <class 'buddy.bdd'> # let's make sure that b is a cube # (depending on how the run was generated you might not need that) c = buddy.bdd_satone(b) # iterate on all variables of a cube assert c != buddy.bddfalse res = [] while c != buddy.bddtrue: ... var = buddy.bdd_var(c) ... h = buddy.bdd_high(c) ... if h == buddy.bddfalse: ... res.append(-var) ... c = buddy.bdd_low(c) ... else: ... res.append(var) ... c = h ... print(res) [0, -1]
Unfortunately, you'll only get variable numbers instead of the actual propositions.
The mapping between atomic propositions and BDD variables is done by the spot.bdd_dict instance returned by run.aut.get_dict(), unfortunately this class does not seem to be completely binded in Python so far, and I'm not overly excited to expose it too much in its current state.
However another way to get the mapping between atomic proposition and BDD variables is to pretend that you register the variables again:
for i in run.aut.ap(): ... print(i, run.aut.register_ap(i)) a 0 b 1
So now you can decode [0, -1] as meaning a&!b.
(no, that is not feature request:) if not possible, I will simply print the label and parse the string, that is not crucial)
In fact the C++ library as a function called spot::bdd_to_formula that would be much cleaner to use. Unfortunately it is not yet binded in Python. I'll make it available in the next release. With this function we can explore boolean labels using the LTL formula interface:
import spot run = spot.translate('a & !b').accepting_run() b = run.prefix[0].label f = spot.bdd_to_formula(b, run.aut.get_dict()) f a & !b f._is(spot.op_And) True len(f) 2 f[0] a f[0]._is(spot.op_ap) True f[1] !b f[1]._is(spot.op_Not) True f[1][0] b
(the above will only work in the next release) -- Alexandre Duret-Lutz
Ayrat Khalimov <ayrat.khalimov@gmail.com> writes:
O, found the answer. According to the implementation of the function spot::bdd_to_formula, any formula of transition.cond is of the form of "sum of products", so a straightforward traversing of the formula bdd_to_formula(transition.cond) is sufficient.
Exactly. If the top-level if the result is not an Or operator, then the output is a single cube, otherwise is a disjunction of cubes. If you need the result as a BDD, it's faster to use minato_isop directly (bdd_to_formula uses this but additionally has to convert the BDD to a formula).
participants (2)
-
Alexandre Duret-Lutz -
Ayrat Khalimov