26 May
2021
26 May
'21
2:36 p.m.
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(a)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(a)lrde.epita.fr>
wrote:
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