Exploration of State Space in NuSMV Source

Question

I am working on a program correction/synthesis project. My task is to obtain an error trace (counter-example), locate it in the complete state space, and repair the model at that location. I want to implement this as a NuSMV extension.

I have been debugging NuSMV to understand and explore its source code. So far, I have found my way to the creation of the BDD FSM (compile.c line 520). I am trying to find a way to traverse the bdd in order to gain programmatic access to the state space, and thus perform my corrective work upon the model. I have not yet been able to understand the recursive exploration functions NuSMV uses to verify properties via the bdd fsm.

I would like to know how i can traverse the bdd structure so I can visualise it through tools like dot. I would also like to know if such or smilar visualisations have already been made (I have searched but come up empty). Secondly, I would like to verify whether the direction I have taken up is the right one, or if there is a better way to obtain the complete state space of a given model, and explore it, especially with regards to a counter-example obtained through NuSMV.

Answer 1

This is an answer about ways to work with binary decision diagrams (BDDs) using CUDD other than via NuSMV, so focusing on the question's second part.

About symbolic algorithms for investigating a state space, the paper "Algorithmic verification of linear temporal logic specifications" by Kesten, Pnueli, and Raviv (ICALP '98, DOI: 10.1007/BFb0055036) is a good introduction, which covers counterexample construction.

One possibility for visualizing BDDs is working in Python, using Cython bindings to 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()

This approach uses dd, which can be installed using pip, with pip install dd. Documentation can be found here. Looking at the (internal) module dd._abc may also be informative (this serves as a specification; the name "abc" alludes to abstract base classes in Python). (Pure Python suffices for smaller problems, and CUDD is useful for larger problems).

There are two kinds of traversals relevant to the question:

1. traversal of the graph of BDD
2. traversal of the graph that has states as nodes and steps as edges.

These are discussed separately below.

Traversing the graph of a BDD

Depth-first traversal is more common than breath-first when working with BDDs. For the interface of dd.cudd and dd.autoref such a traversal is:

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()

Complemented edges need also to be taken into account when working with BDDs (using CUDD or similar libraries). The attribute u.negated provides this information.

The function dd.bdd.copy_bdd is a pure Python example of traversing a BDD. This function manipulates BDDs directly through a "low level" interface that is wrapped by dd.autoref to look the same as dd.cudd.

Traversal of a state graph

The script dd/examples/reachability.py shows how to compute from which states a given set of states can be reached in a finite number of steps.

The package omega is more convenient than dd for developing BDD-based algorithms related to system behaviors. The script omega/examples/reachability_solver demonstrates a reachability computation using omega.

A basic example of forward reachability using omega == 0.3.1 follows:

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()

Comparing omega with dd:

• omega supports variables and constants, and integer values for these (the relevant module is omega.symbolic.temporal). Variables represent state changes, for example x and x'. Constants remain unchanged through a system's behavior.

• dd supports only Boolean-valued variables (omega uses Boolean-valued variables to represent integer-valued variables, and so represent predicates as BDDs via dd; the bitblasting is done in the module omega.logic.bitvector).

Several fixpoint operators are implemented in omega.symbolic.fixpoint. These operators can be used for model checking or temporal synthesis. The module omega.logic.past includes translations of temporal operators that are relevant to symbolic model checking (also known as temporal testers).

Documentation of omega can be found here.

Further comments

I used the term "step" above to refer to a pair of consecutive states that represents a change of state allowed by the specification. The TLA+ language, and steps, flexible and rigid variables, and other useful concepts are described in Leslie Lamport's book Specifying Systems.

A collection of formal verification software is listed at https://github.com/johnyf/tool_lists/.

In my experience, working at the Python level, with only the BDD manager at the C level, is an efficient approach that leads to readable code, and clearer algorithms.