bdd2dfa 0.2.3

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. time: A number between #vars and 0. This number indicates the number of decisions left to be made.
2. node: A reference to the internal BDD node given by dd.
3. 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

For example,

assert qdd.start.parity is True
assert qdd.start.time == 3
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 time attribute.

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