Converting Automaton to MDD?

[glarange]

Is it possible to convert the Automoton 'aut' below to an MDD? If so, how?
Thanks, Gui

from omega.symbolic import temporal as trl

aut = trl.Automaton()
aut.declare_variables(x=(1, 3), y=(-3, 3))
u = aut.add_expr('x = 1 /\ y \in 1..2')

code from: tulip-control/dd#71 (comment)

[johnyf]

By using the function from dd that is mentioned in that issue.

[glarange]

Which one, could you name it once more please? For example, I tried v, vmap =_mdd.bdd_to_mdd(aut, dvars) but this didn't work. Got AttributeError: 'Automaton' object has no attribute 'collect_garbage'.
Thanks.

from omega.symbolic import temporal as trl
from dd import mdd as _mdd
from dd.bdd import BDD as bdd

aut = trl.Automaton()

aut.declare_variables(x=(0, 3), y=(0, 1))
u=aut.add_expr('(x = 0 /\ y = 0) \/ (x = 2 /\ y = 1) \/ (x = 1 /\ y = 0)')
#aut.bdd.incref(u)

aut.bdd.dump('example_bdd_integers.pdf',[u])

dvars = dict(
    x=dict(level=1, len=4, bitnames=['x0', 'x1']),
    y=dict(level=0, len=2, bitnames=['y0']))

v, vmap =_mdd.bdd_to_mdd(aut, dvars)

[johnyf]

The argument to the function bdd_to_mdd needs to be an instance of dd.bdd.BDD, and the bitnames need to be as those in the values of aut.vars. With these changes, the following code runs without errors:

from omega.symbolic import temporal as trl
from dd import mdd as _mdd
import dd.autoref

aut = trl.Automaton()
aut.bdd = dd.autoref.BDD()

aut.declare_constants(x=(0, 3), y=(0, 1))
u = aut.add_expr(r'(x = 0 /\ y = 0) \/ (x = 2 /\ y = 1) \/ (x = 1 /\ y = 0)')

aut.bdd.dump('example_bdd_integers.pdf', [u])

dvars = dict(
    x=dict(level=1, len=4, bitnames=['x_0', 'x_1']),
    y=dict(level=0, len=2, bitnames=['y_0']))

v, vmap = _mdd.bdd_to_mdd(aut.bdd._bdd, dvars)

[glarange]

Thanks. The r in the expression
u = aut.add_expr(r'(x = 0 /\ y = 0) \/ (x = 2 /\ y = 1) \/ (x = 1 /\ y = 0)')
is just a typo and can be removed, I think.

[johnyf]

The "r" prefix in the Python string r'(x = 0 /\ y = 0) \/ (x = 2 /\ y = 1) \/ (x = 1 /\ y = 0)' signifies a raw string and in this case is necessary.