bdd2dfa 0.2.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

dfa = to_dfa(bexpr)

assert len(dfa.states()) == 7

assert dfa.label([1, 1, 1, 1])      # BDD rejects.
assert not dfa.label([0, 1, 1, 1])  # BDD accepts.
assert dfa.label([1, 1]) is None    # Non-leaf node.