0. BDD->MDD wrapper

TBD

1. MDD manager

- projection (variable)
  Given variable x, return the MDD representing the function f(x)=x; that
  is, a single node u where child(u, i)=i
- constant (value)
  Return the constant function f(x)=value
- equals (f, value)
  Return the function g where g(x)=1 if f(x)=value, 0 otherwise.
- apply(f, g, function)
  Return the function h where h(x)=function(f(x), g(x))
- apply(f, function)
  Return the function h where h(x)=function(f(x))
- existentialAbstract (f, list-of-variables)
  Existentially abstract the given list of variables out of f; the
  resultant does not depend on any of the given variables.
- exchange (f, list1-of-variables, list2-of-variables)


2. The Wrapper

Constants:

  -prestate-variables (array of variables)
  -poststate-variables (array of variables)

    These two arrays encode the relation between primed and unprimed variables.

    Example: there are two state variables, x and y, interleaved. Then:

       prestate[1] = 1
       prestate[2] = 3
       poststate[1] = 2
       poststate[2] = 4

Model-checking:
- conjunction(f, g)
  Apply the meet of the lattice to f and g
- disjunction(f, g)
  Apply the join of the lattice to f and g
- projection (variable)
  Directly wraps projection() in DD package
- equals (f, value)
  Directly wraps equals() in DD package
- complement(f, g) 
  Apply the quasi-complement of the lattice to f
- backwardImage (R, g)
  Take the backward image of g along R by:
     1. Calling exchange(g, prestate-variables, poststate-variables)
- exchange(f, list1-of-variables, list2-of-variables)
   This is still used in model-building.