model-checking - 如何用 CUDD 包替换 BDD 中的一些变量？

Question

假设DdManager有四个变量：x, y, x', y'并且我有一个由xand构建的 BDD y。现在我想更改x为x', y,y'即获得由x'and构建的相同 BDD y'。

我怎样才能使用 CUDD 包得到这个？当我想实现模型检查算法时遇到了这个问题。我想知道如何实现这个操作或者我是否误解了符号模型检查算法？非常感谢！

Answer 1

您可以使用函数来执行此操作Cudd_bddSwapVariables。它获取以下参数：

1. BDD 经理
2. 您希望将变量替换为其他变量的 BDD。
3. 第一个变量数组（由也Cudd_bddNewVar将返回的 BDD 节点表示）
4. 第二个变量数组
5. 正在交换的变量数。

您将需要自己分配和释放数组。

Answer 2

使用 Cython 绑定到包dd中包含的 CUDD 的变量替换示例：

from dd import cudd

bdd = cudd.BDD()  # instantiate a shared BDD manager
bdd.declare("x", "y", "x'", "y'")
u = bdd.add_expr(r"x \/ y")  # create the BDD for the disjunction of x and y
rename = dict(x="x'", y="y'")
v = bdd.let(rename, u)  # substitution of x' for x and y' for y
s = bdd.to_expr(v)
print(s)  # outputs:  "ite(x', TRUE, y')"

# another way to confirm that the result is as expected
v_ = bdd.add_expr(r"x' \/ y'")
assert v == v_