Python library for converting binary decision diagrams to automata.
A simple python wrapper around Binary Decision Diagrams (BDDs) to interpret them as Deterministic Finite Automata (DFAs).
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
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
# 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:
node: A reference to the internal BDD node given by
ddsupports 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
debt: Number of inputs needed before this node can transition. Required since
BDDedges can skip over irrelevant decisions.
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
bdd = to_dfa(bexpr, qdd=False)
DFA uses a similar state as the
QDD case, but does not have a
debt attribute. Useful when one just wants to walk the
note The labeling alphabet also only returns the decision variable/truth assignment.
dfa package was installed with the
draw option, we can
visualize the difference between
bdd by exporting to a
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
and the following for
Release history Release notifications | RSS feed
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.