Исследование пространства состояний в исходном коде NuSMV

Это ответ о способах работы с бинарными диаграммами решений (BDD) с использованием CUDD, отличного от NuSMV, поэтому основное внимание уделяется второй части вопроса.

О символических алгоритмах исследования пространства состояний см. статью Алгоритмическая проверка спецификации линейной темпоральной логики Кестена, Пнуэли и Равива (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('(x /\ y) \/ ~ z')
    bdd.dump('foo.pdf', [u])


if __name__ == '__main__':
    dump_pdf_cudd()

Этот подход использует dd, который можно установить с помощью pip с pip install dd. Документацию можно найти здесь. Просмотр (внутреннего) модуля dd._abc также может быть информативным (это служит спецификацией; название abc намекает на абстрактные базовые классы на Питоне). (Чистого Python достаточно для небольших задач, а CUDD полезен для более крупных задач).

Есть два вида обходов, имеющих отношение к вопросу:

1. обход графа BDD
2. обход графа, который имеет состояния в качестве узлов и шаги в качестве ребер.

Они обсуждаются отдельно ниже.

Обход графа BDD

При работе с BDD обход в глубину более распространен, чем обход в глубину. Для интерфейса dd.cudd и dd.autoref такой обход:

from dd import autoref as _bdd


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


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


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


if __name__ == '__main__':
    demo_bdd_traversal()

Дополненные ребра также необходимо учитывать при работе с BDD (используя CUDD или аналогичные библиотеки) . Атрибут u.negated предоставляет эту информацию.

Функция dd.bdd.copy_bdd — это чистый пример Python. обхода BDD. Эта функция манипулирует BDD напрямую через низкоуровневый интерфейс, обернутый dd.autoref, чтобы он выглядел так же, как dd.cudd.

Обход графа состояний

Сценарий dd/examples/reachability.py показывает, как вычислять из каких состояний заданный набор состояний может быть достигнут за конечное число шагов.

Пакет omega более удобен, чем dd, для разработки алгоритмов на основе BDD, связанных с поведением системы. Сценарий omega/examples/reachability_solver демонстрирует вычисление достижимости с использованием omega.

Ниже приведен базовый пример доступности вперед с использованием omega == 0.3.1:

from omega.symbolic import temporal as trl
from omega.symbolic import 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('{n} states are reachable'.format(n=n))


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 использует переменные с логическими значениями для представления переменных с целочисленными значениями и, таким образом, представляет предикаты в виде BDD через dd; обработка битов выполняется в модуле omega.logic.bitvector).

Несколько операторов фиксированной точки реализованы в omega.symbolic.fixpoint. Эти операторы можно использовать для проверки модели или временного синтеза< /а>. Модуль omega.logic.past включает переводы темпоральных операторов, относящихся к проверке символьной модели (также известных как временные тестировщики).

Документацию по omega можно найти здесь.

Дальнейшие комментарии

Я использовал термин «шаг» выше для обозначения пары последовательных состояний, которые представляют собой изменение состояния, разрешенное спецификацией. Язык и шаги TLA+, гибкие и жесткие переменные и другие полезные концепции описаны в книге Лесли Лэмпорт Указание систем.

Набор программного обеспечения для формальной проверки указан по адресу https://github.com/johnyf/tool_lists/. .

По моему опыту, работа на уровне Python с использованием только BDD-менеджера на уровне C является эффективным подходом, который приводит к читабельному коду и более четким алгоритмам.