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:
- traversal of the graph of BDD
- 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.
