8 Mar
2017
8 Mar
'17
2:35 p.m.
Hi Ayrat,
On Wed, Mar 8, 2017 at 11:32 AM, Ayrat Khalimov
<ayrat.khalimov(a)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