Python library for converting binary decision diagrams to automata.
Project description
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 the label of non-leaf states in the original BDD is None
and
all leaves self loop.
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.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
assert qdd.label([1, 1, 1, 1]) # QDD rejects.
assert qdd dfa.label([0, 1, 1, 1]) # QDD accepts.
assert qdd.label([1, 1]) is None # Non-leaf node.
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 nodedebt
: 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
.
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
:
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.