NuSMV源代码中状态空间的探索

Question

我正在做一个程序更正/合成项目。我的任务是获取错误跟踪(反例)，在完整的状态空间中定位它，并在该位置修复模型。我想把它实现为一个NuSMV扩展。

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

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

Answer 1

这是一个关于如何使用CUDD而不是通过NuSMV来处理二叉决策图(BDD)的答案，因此请重点关注问题的第二部分。

关于调查状态空间的符号算法，Kesten，Pnueli和Raviv的论文"Algorithmic verification of linear temporal logic specifications" (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 install dd使用pip安装。文档可以在here上找到。查看(内部)模块dd._abc也可能是为了提供信息(这是一种规范；名称"abc“在Python语言中暗指abstract base classes )。(纯Python适用于较小的问题，而CUDD适用于较大的问题)。

​

​

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

以状态为节点、步骤为边的图的BDD

• traversal图的

1. 遍历。

这些将在下面单独讨论。

遍历BDD的图形

在使用BDDs时，深度优先遍历比呼吸优先更常见。对于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或类似的库)时，也需要考虑Complemented edges。attribute u.negated提供了此信息。

函数dd.bdd.copy_bdd是一个遍历BDD的纯Python示例。此函数通过一个“低级”接口直接操作dd.cudd，该接口由dd.autoref包装以使其外观与BDD相同。

状态图的遍历

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

在开发与系统行为相关的基于边界发现的算法时，omega软件包比dd更方便。脚本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.logic.bitvector).

中，omega使用布尔值变量来表示整数值变量，因此通过dd将谓词表示为BDD

在omega.symbolic.fixpoint中实现了几个定点运算符。这些运算符可用于模型检查或temporal synthesis。模块omega.logic.past包括与符号模型检查(也称为)相关的时间运算符的翻译。

可以在here中找到omega的文档。

进一步的评论

我使用上面的术语“步骤”来表示一对连续的状态，它们表示规范允许的状态更改。Leslie Lamport的书Specifying Systems中描述了TLA+语言、步骤、灵活变量和刚性变量以及其他有用的概念。

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

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