Lecture notes introducing Binary Decision Diagrams and an implementation of a BDD package in Standard ML is freely available by World Wide Web and anonymous ftp at the addresses below. The lecture notes were used in a course at the Technical University of Denmark, autumn 1994. The BDD package is a solution to one of the projects proposed in the lecture notes. As an application of the package it is shown how to compute and count the reachable states of Milner's Scheduler for various numbers of cyclers. (For 40 cyclers the count is 65970697666560 !)
The BDD lecture notes and implementation are available (under Lecture Notes), or by anonymous ftp:
The files must be uncompressed by `gunzip' or `zip' and the .tar-file unpacked by `tar xf'.
Comments and bug reports are very welcome and can be directed to:
Henrik Reif Andersen
E-mail: hra@id.dtu.dk
WWW
Department of Computer Science, Bld. 344
Technical University of Denmark,
DK-2800 Lyngby, Denmark