model-checking - CUDD:ZDD 的量化

Question

我正在使用 CUDD (https://github.com/ivmai/cudd) 使用 bdd 和 zdd 功能进行模型检查，我想知道如何量化 zdds。
对于 bdd，有 bddExistAbstract 和 bddUnivAbstract 函数(参见 http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/cuddAllDet.html#Cudd_bddUnivAbstract)。
该手册说，这些函数普遍地和存在地从 bdd 中抽象出给定的变量(以封面形式)。我不太清楚“抽象出来”是什么意思，因此我坚持弄清楚量化如何改变 zdds。
你们能帮忙吗？谢谢。

Answer 1

Python 包 dd 实现到 CUDD 的 Cython 接口(interface)，该接口(interface)通过量化扩展了 CUDD 的 ZDD 功能。例如，要在 ZDD 上使用存在量化:

from dd import cudd_zdd

zdd = cudd_zdd.ZDD()  # create a ZDD manager
zdd.declare('x', 'y')  # add variables to the manager
u = zdd.add_expr(r'x /\ y')  # create a BDD `u` for the expression x /\ y
v = zdd.exist(['y'], u)  # quantify over variable y, i.e., compute \E y:  x /\ y
>>> zdd.to_expr(v)  # convert to an expression as string
'x'

ZDD 量化的实现可以在以下位置找到:
https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1999-L2172
并且出于开发目的也存在许多 Python 级别的实现:
https://github.com/tulip-control/dd/blob/24ec9eba335c173e1fe0367a9ac25ec201dee1b5/dd/cudd_zdd.pyx#L1387-L1544
包 dd可以从 PyPI 安装与 pip install dd .这将在 Linux 上安装 CUDD 绑定(bind)。在 macOS 上，与 CUDD 的绑定(bind)需要从 dd 的源代码编译。 ，因此 macOS 的安装变为:

pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd --cudd_zdd

如文件 README.md 中所述.