bdd2dfa 0.4.0

Python library for converting binary decision diagrams to automata.

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
• 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.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:

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.

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: