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 quasireduced 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
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 Nonleaf 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:

node
: A reference to the internal BDD node given bydd
. 
parity
:dd
supports Edge NegatedBDD
s, where some edges point to a Boolean function that is the negation of the Boolean function the node would point to in a standardBDD
. Parity value determines whether or not the node 
debt
: Number of inputs needed before this node can transition. Required sinceBDD
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
: