Skip to main content

Python library for converting binary decision diagrams to automata.

Project description


Build Status codecov PyPI version License: MIT

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


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.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'


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, "")
write_dot(bdd, "")

Compiling using the dot command yields the following for

qdd image

and the following for

bdd image

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

bdd2dfa-0.2.3.tar.gz (4.5 kB view hashes)

Uploaded Source

Built Distribution

bdd2dfa-0.2.3-py3-none-any.whl (4.3 kB view hashes)

Uploaded Python 3

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page