tulip-control / dd

Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
https://pypi.org/project/dd
Other
178 stars 39 forks source link

More examples with MDDs #69

Closed glarange closed 3 years ago

glarange commented 3 years ago

Multi-state reliability with MDDs: An example

I'm working with multi-state reliability using MDDs. Analogous to binary reliability and BDDs. Each standalone component of the system is represented by a different variable $x_i$. Each component $x_i$ can be in a state with a range given by an integer number $n_i$, where each state is encoded by a set of bits $x_i0, xi1,...,c= x{iki}$ , where $x{ik_i}$ is the MSB. In this example, we use binary encoding so that $n_i<2^{k_i}$.

The top event is then represented by a sum of products of the states. The difference is that the factors (states) in the products are no longer necessarily independent. For example,

$x_0 = 0,1,2$ and $x_1 = 0,1,2,3, x_2 = 0,1,2,3$

$x0= x{00} x_{01} , x1= x{10}x_{11} and x_2= x{20}x{21}$

$Top=x{00}+x{10}x{11}+ x{20}$.

And the system would fail in this example if $x{00}=1$, or $x{10}x{11}=1$ or $x{21}=0$. Or equivalently, if $x_0=1$ or $x_1=3$ or $x_2=0,2$.

Then my attempt to use mdd to represent this (below) fails due to an "assertion error" on the last command. Can you tell me what I'm doing wrong, please?

from dd.bdd import BDD
from dd import mdd as _mdd

bits = dict(x00=0, x01=1, x10=2, x11=3, x20=4, x21=5)
bdd = BDD(bits)
u = bdd.add_expr('x00 \/ x10 /\ x11 \/~x20')
bdd.incref(u)

# convert BDD to MDD
ints = dict(
    x0=dict(level=0, len=3, bitnames=['x00','x01']),
    x1=dict(level=1, len=4, bitnames=['x10','x11']),
    x2=dict(level=2, len=4, bitnames=['x20', 'x21']))
mdd, umap = _mdd.bdd_to_mdd(bdd, ints)
johnyf commented 3 years ago

The assertion error is caused by len=3 for x0. Using:

ints = dict(
    x0=dict(level=0, len=4, bitnames=['x00','x01']),

avoids the error, and the conversion by the function _mdd.bdd_to_mdd completes successfully. The necessity for len=4 follows from the use of two bits ('x00' and 'x01') for the BDD representation. The presence of two bits means that there result 4 paths in the BDD, and these paths are to be transferred to the MDD. So the integer-valued variable x0 that corresponds to the bitfield ['x00', 'x01'] ranges over 4 values (not 3). This observation applies to the function _mdd.bdd_to_mdd in general, i.e., the MDD variables would have lengths of the form 2**k for some k \in Nat (where Nat the set of natural numbers).