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.

Table of Contents

• Installation
• Usage

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 BDDs, 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: