0

@DCTLib，您还记得下面的讨论吗？你提出了一个递归方程，这是正确的方法。

Cudd_PrintMinterm，访问产品总和中的各个最小项

现在，我正在考虑多状态可靠性，我们可以不失败或失败到 n-1 个不同的状态，其中 n >= 2。Tulip-dd 实现 MDD，如下所述：

https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd

https://github.com/tulip-control/dd/issues/71

https://github.com/tulip-control/dd/issues/66

在下图中的图中，我们定义了一个 MDD，声明如下：

aut.declare_variable(x=(0,3)) u = aut.add_expr('x=i')

多值变量 (MSV) x、x=0、x=1、x=2 或 x=3 的每个值/状态都会导致特定的 BDD，如下图所示，采用四态这里以变量 x 为例。表示法是状态 0 代表正常状态​​，x 可以失败到不同的状态 1、2 和 3。失败概率在下表中分配。在下面的 BDD 中，我们（以及 tulip）使用二进制编码，带有两个位 x_1 和 x_0 来表示 MSV 的每个状态/值。最低有效位 (LSB)，即 x_0，始终是祖先。下面的每个 BDD 图都是特定值或状态的表示。

为了量化特定状态的 BDD，即顶部节点，我们必须知道二进制变量 x_0 和 x_1 在 BDD 中采用不同分支（then or else）的概率。这些分支概率没有直接给出，需要根据BDD结构计算。

这里的关键是在计算父节点概率之前必须知道子节点概率和父节点的分支概率。在之前的 BDD 量化中，我们在计算节点 x_1 概率时，就知道了从节点 x_1 到叶子节点的分支概率。我们不需要知道节点 x_1 是如何连接到节点 x_0 的。现在，对于这个四态变量 x，我们需要知道节点 x_1 是如何连接到节点 x_0（代表最低有效位的二进制变量）来确定从节点 x_1 到叶节点的分支概率。问题是如何实现这一点？

Here’s one attempt that falls short:

import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()
# Example of function that returns branch probabilities
def prntr(v, pvars):
    
    assert sum(pvars)==1.0,"Probs must add to 1!"

    if (v.high).var == 'x_1':
        if (v.low) == aut.true:
            return pvars[1] + pvars[3], pvars[1]
        else:
            return pvars[1] + pvars[3], pvars[3]
    if (v.low).var == 'x_1':
        if (v.low).negated:
            return pvars[1] + pvars[3], pvars[0]
        else:
            return pvars[1] + pvars[3], pvars[2]
aut.declare_variables(x=(0, 3))
u=aut.add_expr('x = 3')
pvars = np.array([0.1, 0.2, 0.3, 0.4])
prntr(u,pvars)

在此处输入图像描述

在此处输入图像描述

4

1 回答 1

1

这里的关键是在计算父节点概率之前必须知道子节点概率和父节点的分支概率。

对，就是这样。在这种情况下，完全递归的自下而上计算，就像通常使用 BDD 完成的那样，由于您编写的原因将无法工作。

但是，当您将共同形成状态的变量视为块时，该方法将再次开始起作用。因此，在您用于概率计算的递归函数中，每当您遇到块的变量时，您将相同状态组件的节点和后继节点视为一个块，并且仅在遇到不属于该块的节点时才会递归。

请注意，这种方法要求状态的变量在变量排序中连续出现。对于 CUDD 库，您可以约束自动变量重新排序以保证这一点。

以下代码是您实现此想法的修改：

#!/usr/bin/env python3
import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()

# Example of function that returns branch probabilities
# Does not yet use result caching and does not yet support assigning probabilities 
# to more than one state variable set
def prntr(v, pvars):
    
    assert abs(sum(pvars)-1.0)<=0.0001,"Probs must add to 1!"
    
    if v == aut.true:
        return 1.0
    elif v == aut.false:
        return 0.0
        
    if v.var in ["x_0","x_1"]:
        thisSum = 0.0
        # Compute probabilities
        for i,p in enumerate(pvars):
            
            # Find successor
            # Assuming that x_2 always comes after x_1
            thisV = v
            negate = thisV.negated
            if thisV.var == 'x_0':
                if i & 1:
                    thisV = thisV.high
                else:
                    thisV = thisV.low
                    negate = negate ^ thisV.negated
            if thisV.var == 'x_1':
                if i & 2:
                    thisV = thisV.high
                else:
                    thisV = thisV.low
            if negate:
                thisSum += p*prntr(~thisV, pvars)
            else:
                thisSum += p*prntr(thisV, pvars)
        
        return thisSum

    # TODO: What is the semantics for variables outside of the current block?
    return 0.5*prntr(v.high, pvars) + 0.5*prntr(v.low, pvars)

pvars = np.array([0.1, 0.2, 0.3, 0.4])
aut.declare_variables(x=(0, 3))
u= aut.add_expr('x = 0')
print(prntr(u,pvars))
u2 = aut.add_expr('x = 3') | aut.add_expr('x = 2')
print(prntr(u2,pvars))
于 2021-04-05T12:42:03.587 回答