2

我正在做一个程序校正/综合项目。我的任务是获取错误轨迹（反例），将其定位在完整的状态空间中，并在该位置修复模型。我想将其实现为 NuSMV 扩展。

我一直在调试 NuSMV 以了解和探索它的源代码。到目前为止，我已经找到了创建 BDD FSM 的方法（compile.c 第 520 行）。我试图找到一种遍历 bdd 的方法，以便以编程方式访问状态空间，从而对模型执行我的纠正工作。我还不能理解 NuSMV 用来通过 bdd fsm 验证属性的递归探索函数。

我想知道如何遍历 bdd 结构，以便通过 dot 等工具对其进行可视化。我还想知道是否已经制作了这样或类似的可视化（我已经搜索过但没有找到）。其次，我想验证我所采取的方向是否正确，或者是否有更好的方法来获得给定模型的完整状态空间，并探索它，特别是关于获得的反例通过 NuSMV。

4

1 回答 1

1

这是关于使用 CUDD 而非通过 NuSMV 处理二元决策图 (BDD) 的方法的答案，因此请关注问题的第二部分。

关于用于研究状态空间的符号算法，Kesten、Pnueli 和Raviv 的论文“线性时序逻辑规范的算法验证” （ICALP '98，DOI： 10.1007/BFb0055036）是一个很好的介绍，其中涵盖了反例构建。

可视化 BDD 的一种可能性是在 Python 中工作，使用 Cython 绑定到 CUDD：

from dd import cudd


def dump_pdf_cudd():
    bdd = cudd.BDD()
    bdd.declare('x', 'y', 'z')
    u = bdd.add_expr(r'(x /\ y) \/ ~ z')
    bdd.dump('foo.pdf', [u])


if __name__ == '__main__':
    dump_pdf_cudd()

这种方法使用dd，可以安装使用pip，与pip install dd。文档可以在这里找到。查看（内部）模块dd._abc也可能会提供信息（这用作规范；名称“abc”暗指 Python 中的抽象基类）。（纯 Python 足以解决较小的问题，而 CUDD 适用于较大的问题）。

在此处输入图像描述

有两种与问题相关的遍历：

  1. BDD图的遍历
  2. 遍历以状态为节点、以步骤为边的图。

这些将在下面单独讨论。

遍历 BDD 的图

在使用 BDD 时，深度优先遍历比呼吸优先更常见。对于dd.cudd和dd.autoref这样一个遍历的接口是：

import dd.autoref as _bdd


def demo_bdd_traversal():
    bdd = _bdd.BDD()
    bdd.declare('x', 'y')
    u = bdd.add_expr(r'x /\ y')
    print_bdd_nodes(u)


def print_bdd_nodes(u):
    visited = set()
    _print_bdd_nodes(u, visited)


def _print_bdd_nodes(u, visited):
    # leaf ?
    if u.var is None:
        print('leaf reached')
        return
    # non-leaf
    # already visited ?
    if u in visited:
        return
    # recurse
    v = u.low
    w = u.high
    # DFS pre-order
    print(f'found node {u}')
    _print_bdd_nodes(v, visited)
    # DFS in-order
    print(f'back to node {u}')
    _print_bdd_nodes(w, visited)
    # DFS post-order
    print(f'leaving node {u}')
    # memoize
    visited.add(u)


if __name__ == '__main__':
    demo_bdd_traversal()

使用 BDD（使用 CUDD 或类似库）时，还需要考虑互补边。该属性u.negated提供此信息。

该函数dd.bdd.copy_bdd是遍历 BDD 的纯 Python 示例。此函数通过一个“低级”接口直接操作 BDD，该接口dd.autoref由dd.cudd.

状态图的遍历

该脚本dd/examples/reachability.py显示了如何计算从哪些状态可以在有限的步骤中达到给定的一组状态。

该软件包omega比dd开发与系统行为相关的基于 BDD 的算法更方便。该脚本omega/examples/reachability_solver演示了使用omega.

前向可达性的基本示例omega == 0.3.1如下：

import omega.symbolic.temporal as trl
import omega.symbolic.prime as prm


def reachability_example():
    """How to find what states are reachable."""
    aut = trl.Automaton()
    vrs = dict(
        x=(0, 10),
        y=(3, 50))
    aut.declare_variables(**vrs)
    aut.varlist = dict(
        sys=['x', 'y'])
    aut.prime_varlists()
    s = r'''
        Init ==
            /\ x = 0
            /\ y = 45

        Next ==
            /\ (x' = IF x < 10 THEN x + 1 ELSE 0)
            /\ (y' = IF y > 5 THEN y - 1 ELSE 45)
        '''
    aut.define(s)
    init = aut.add_expr('Init', with_ops=True)
    action = aut.add_expr('Next', with_ops=True)
    reachable = reachable_states(init, action, vrs, aut)
    n = aut.count(reachable, care_vars=['x', 'y'])
    print(f'{n} states are reachable')


def reachable_states(init, action, vrs, aut):
    """States reachable by `action` steps, starting from `init`."""
    operator = lambda y: image(y, action, vrs, aut)
    r = least_fixpoint(operator, init)
    assert prm.is_state_predicate(r)
    return r


def image(source, action, vrs, aut):
    """States reachable from `source` in one step that satisfies `action`."""
    u = source & action
    u = aut.exist(vrs, u)
    return aut.replace_with_unprimed(vrs, u)


def least_fixpoint(operator, target):
    """Least fixpoint of `operator`, starting from `target`."""
    y = target
    yold = None
    while y != yold:
        yold = y
        y |= operator(y)
    return y


if __name__ == '__main__':
    reachability_example()

比较：omega_dd

  • omega支持变量和常量，以及它们的整数值（相关模块是omega.symbolic.temporal）。变量表示状态变化，例如x和x'。常数通过系统的行为保持不变。

  • dd仅支持布尔值变量（omega使用布尔值变量来表示整数值变量，因此将谓词表示为ddBDDs via ；位爆破在模块中完成omega.logic.bitvector）。

几个定点运算符在omega.symbolic.fixpoint. 这些算子可用于模型检查或时间合成。该模块omega.logic.past包括与符号模型检查相关的时间运算符的翻译（也称为时间测试器）。

的文档omega可以在这里找到。

进一步的评论

我在上面使用了术语“步骤”来指代一对连续的状态，它们表示规范允许的状态变化。Leslie Lamport 的《指定系统》一书中描述了 TLA+ 语言、步骤、柔性和刚性变量以及其他有用的概念。

https://github.com/johnyf/tool_lists/列出了形式验证软件的集合。

根据我的经验，在 Python 级别工作，只有 C 级别的 BDD 管理器是一种有效的方法，可以产生可读的代码和更清晰的算法。

于 2020-09-05T21:15:30.670 回答