# bdd2dfa Release 1.0.10

Python library for converting binary decision diagrams to automata.

MIT
Install
``` pip install bdd2dfa==1.0.10 ```

# bdd2dfa

A simple python wrapper around Binary Decision Diagrams (BDDs) to interpret them as Deterministic Finite Automata (DFAs).

The package takes as input a BDD from the `dd` package and returns a DFA from the `dfa` package.

Formally, the resulting `DFA` objects are quasi-reduced BDDs (QDDs) where all leaves self loop and the label of states is a tuple: `(int, str | bool)`, where the first entry determines the number of inputs until this node is active and the second entry is the decision variable of the node or the BDD's truth assignment.

# Installation

If you just need to use `bdd2dfa`, you can just run:

`\$ pip install bdd2dfa`

For developers, note that this project uses the poetry python package/dependency management tool. Please familarize yourself with it and then run:

`\$ poetry install`

# Usage

```# Create BDD

from dd import BDD

manager = BDD()
manager.declare('x', 'y', 'z')
x, y, z = map(manager.var, 'xyz')
bexpr = x & y & z

# Convert to DFA

from bdd2dfa import to_dfa

qdd = to_dfa(bexpr)

assert len(qdd.states()) == 7

# End at leaf node.
assert qdd.label([1, 1, 1]) == (0, True)
assert qdd.label([0, 1, 1]) == (0, False)

# End at Non-leaf node.
assert qdd.label([1, 1]) == (0, 'z')
assert qdd.label([0, 1]) == (1, False)

# leaf nodes are self loops.
assert qdd.label([1, 1, 1, 1]) == (0, True)
assert qdd.label([1, 1, 1, 1, 1]) == (0, True)```

Each state of the resulting `DFA` object has three attribute:

1. `node`: A reference to the internal BDD node given by `dd`.
2. `parity`: `dd` supports Edge Negated `BDD`s, where some edges point to a Boolean function that is the negation of the Boolean function the node would point to in a standard `BDD`. Parity value determines whether or not the node
3. `debt`: Number of inputs needed before this node can transition. Required since `BDD` edges can skip over irrelevant decisions.

For example,

```assert qdd.start.parity is True
assert qdd.start.debt == 0
assert qdd.start.node.var == 'x'```

## BDD vs QDD

`to_dfa` also supports exporting a `BDD` rather than a `QDD`. This is done by toggling the `qdd` flag.

`bdd = to_dfa(bexpr, qdd=False)`

The `DFA` uses a similar state as the `QDD` case, but does not have a `debt` attribute. Useful when one just wants to walk the `BDD`.

note The labeling alphabet also only returns the decision variable/truth assignment.

If the `dfa` package was installed with the `draw` option, we can visualize the difference between `qdd` and `bdd` by exporting to a graphviz `dot` file.

```from dfa.draw import write_dot

write_dot(qdd, "qdd.dot")
write_dot(bdd, "bdd.dot")```

Compiling using the `dot` command yields the following for `qdd.dot`

and the following for `bdd.dot`: