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 variable. The partitioning is conjunctive, with each conjunct representing the transition relation for an atom. Restrictions: Currently, the next operator is not supported.
Last updated on 980624 22h11