8 Mar
2017
8 Mar
'17
11:32 a.m.
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
8 Mar
8 Mar
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
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
26 May
26 May
2:30 p.m.
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
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
10:14 p.m.
Ayrat Khalimov <ayrat.khalimov(a)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).
1351
days inactive
2891
days old
5 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Ayrat Khalimov