The sym package
building symbolic transition relation for a module
By Sriram K. Rajamani
This package contains routines to build the symbolic transition
relation for a module. The task of building the transition
relation has two main components:
1. Selecting a good variable ordering for the BDD package.
2. Parititioning the transition relation
Currently, simple heuristics are used to do both these tasks.
Variable ordering is based on the topological order
generated by the module manager. Based on conventional wisdom,
we keep the "present" and "next" pairs together for each
The partitioning is conjunctive, with each conjunct
representing the transition relation for an atom.
Currently, the next operator is not
Last updated on 980624 22h11