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