Python library for converting binary decision diagrams to automata.

## Project description

# 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 all leaves self loop and the label of states is a tuple: `(int, str | bool)`

, where the first entry determines the number of inputs until this node is active and the second entry is the decision variable of the node or the BDD's truth assignment.

**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 = 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
# End at leaf node.
assert qdd.label([1, 1, 1]) == (0, True)
assert qdd.label([0, 1, 1]) == (0, False)
# End at Non-leaf node.
assert qdd.label([1, 1]) == (0, 'z')
assert qdd.label([0, 1]) == (1, False)
# leaf nodes are self loops.
assert qdd.label([1, 1, 1, 1]) == (0, True)
assert qdd.label([1, 1, 1, 1, 1]) == (0, True)
```

Each state of the resulting `DFA`

object has three attribute:

`node`

: A reference to the internal BDD node given by`dd`

.`parity`

:`dd`

supports Edge Negated`BDD`

s, 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`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`

.

**note** The labeling alphabet also only returns the decision variable/truth assignment.

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`

:

## Project details

## Release history Release notifications | RSS feed

## Download files

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