Skip to main content

Python library for converting binary decision diagrams to automata.

Project description

bdd2dfa

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

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

qdd image

and the following for bdd.dot:

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.

Files for bdd2dfa, version 0.3.2
Filename, size File type Python version Upload date Hashes
Filename, size bdd2dfa-0.3.2-py3-none-any.whl (4.3 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size bdd2dfa-0.3.2.tar.gz (4.5 kB) File type Source Python version None Upload date Hashes View

Supported by

Pingdom Pingdom Monitoring Google Google Object Storage and Download Analytics Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN DigiCert DigiCert EV certificate StatusPage StatusPage Status page